SubsetAntisymmetry Show Code edit
thm (SubsetAntisymmetry () () (→ (∧ (⊆ A B) (⊆ B A)) (= A B))
A B EqualitySubset
(↔ (= A B) (∧ (⊆ A B) (⊆ B A)))
eliminateBiconditionalForward
(→ (∧ (⊆ A B) (⊆ B A)) (= A B))
)
edit