以下は,定理
theorem :: BOOLE'2: X meets Y iff ex x st x in X /\ Y proof hereby assume X meets Y; then X /\ Y <> {} by Def7; then consider x such that A1: x in X /\ Y by Def1; take x; thus x in X /\ Y by A1; end; given x such that A2: x in X /\ Y; X /\ Y <> {} by A2,Def1; hence thesis by Def7; end;
証明は,