比較可能な集合

以下の記述は,集合$X$と$Y$が集合の抱合関係 として比較可能なこと,すなわち

$$(X \subseteq Y) \ or \ (Y \subseteq X)$$

が成り立つことを, $are_c=-comparable$という 述語として定義しています。

 pred X,Y are_c=-comparable means
  X c= Y or Y c= X;
 reflexivity;
 symmetry;

 reflexivity;

は,$X$と$X$自身が比較可能であること ($X \subseteq X$が成り立っていますので)

 symmetry;

は,$X$と$Y$が比較可能であれば, $Y$と$X$も比較可能であることを表しています。 実際,

$$(X \subseteq Y) \ or \ (Y \subseteq X)$$

なら

$$(Y \subseteq X) \ or \ (X \subseteq Y)$$

が成り立っています。