定理$BOOLE'1$

以下は,定理

$$X とYは交わる \Leftrightarrow (\exists x)(x \in X \ and \ x \in Y)$$

の証明です。

theorem BOOLE'1: :: BOOLE'1:
  X meets Y iff ex x st x in X & x in 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 & x in Y by Def3,A1;
 end;
 given x such that
A2: x in X & x in Y;
  x in X /\ Y by Def3,A2;
  then X /\ Y <> {} by Def1;
 hence thesis by Def7;
end;

証明は,

$$X とYは交わる$$

を仮定すると,$Def7$から,

$$X \cap Y \neq \phi$$

よって,$Def1$により,

$$A1:x \in X \cap Y$$

となる$x$が存在し,このような$x$を選れべば, $A1$と$Def1$により,

$$x \in X \ and \ x \in Y$$

となり,

$$(\exists x)(x \in X \ and \ x \in Y)$$

が示されます。逆に,

$$(\exists x)(x \in X \ and \ x \in Y)$$

を仮定すれば,

$$A2:x \in X \ and \ x \in Y$$

となる$x$を選ぶことができ,$Def3,A2$から

$$x \in X \cap Y$$

が成り立ち従って,$Def1$により,

$$X \cap Y \neq \phi$$

が示され,これと$Def7$から証明終了です。