真部分集合

以下の記述は,集合$X$が$Y$の部分集合で,かつ,$Y$と等しく ないこと,すなわち

$$(X \subset Y) \ and \ X \neq Y$$

が成り立つことを「集合$X$は集合$Y$の真部分集合」であるという 述語として定義しています。 部分集合の場合$c=$($\subseteq$)を用いましたので真部分集合には $c<$を用いています。(数学の教科書では$\subset$などが使われて います。)

 pred X c< Y means
  X c= Y & X <> Y;
 irreflexivity;

 irreflexivity;

は,$c=$($\subseteq$)の場合と異なり,

$$X \subset X$$

は成り立たないことを表しています。 これは

$$(X \subset X) \ and \ X \neq X$$

を意味しますので成り立ちません。