buildMembershipLLInConsequent Show Code edit
thm (buildMembershipLLInConsequent ()
(H (→ antecedent (= B0 B1)))
(→ antecedent (↔ (∈ A B0) (∈ A B1)))
H
(→ antecedent (= B0 B1))
B0 B1 A MembershipBuilderLL
(→ (= B0 B1) (↔ (∈ A B0) (∈ A B1)))
applySyllogism
(→ antecedent (↔ (∈ A B0) (∈ A B1)))
)
edit