Theorem: LoVe.Set.subseteq_def (LoVe/LoVelib.lean)

State before:
α : Type
A B : Set α
⊢ A ⊆ B ↔ ∀ (a : α), a ∈ A → a ∈ B
Tactic:
rfl
State after:
no goals