UnorderedPair Show Code edit
thm (UnorderedPair () () (↔ (∈ C (unorderedPair A B)) (∨ (= C A) (= C B)))
A B y UnorderedPairAsAbstraction
(= (unorderedPair A B) (abstract y (∨ (= y A) (= y B))))
C buildMembershipLL
(↔ (∈ C (unorderedPair A B)) (∈ C (abstract y (∨ (= y A) (= y B)))))
C y A B UnorderedPairObject
(↔ (∈ C (abstract y (∨ (= y A) (= y B)))) (∨ (= C A) (= C B)))
applyBiconditionalTransitivity
(↔ (∈ C (unorderedPair A B)) (∨ (= C A) (= C B)))
)
edit