$cluster$の宣言

以下は,集合$\{\}$($\phi$)は$emty$であり, $emty$は集合であること,さらに,空でない集合$non empty$も 集合であることを主張しています。 このような概念の包含関係を示すには$cluster$を用います。

definition
 cluster {} -> empty;
  coherence by Def5;
 cluster empty set;
  existence
   proof {} is empty by Def5; hence thesis; end;
 cluster non empty set;
  existence
   proof consider x;
    x in {x} by TARSKI:def 1;
    then {x} <> {} by Def1;
    then {x} is non empty by Def5; 
    hence thesis;
   end;
end;

 cluster empty set;
  existence
   proof {} is empty by Def5; hence thesis; end;

の記述で,$empty$であるものは集合($set$)であると,概念の包含関係 を示し,さらに,$empty$である対象が少なくとも一つ存在することを 証明しています。$Def5$により, $\{\}$がその$empty$であるものの一つです。

同様に,

 cluster non empty set;
  existence
   proof consider x;
    x in {x} by TARSKI:def 1;
    then {x} <> {} by Def1;
    then {x} is non empty by Def5; 
    hence thesis;
   end;
end;

の記述で,$non empty$であるものは集合($set$)であると,概念の包含関係 を示し,さらに,$non empty$である対象が少なくとも一つ存在することを 証明しています。 実際,$TARSKI:def 1$により,

$$x \in \{x \}$$

が成り立ち,これは$Def1$により,

$$\{x \} \neq \phi$$

従って,$\{x\}$は,$non empty$です。