包含関係の定義

次は,「集合$X$が集合$Y$の部分集合である」 あるは 「集合$X$が集合$Y$に含まれる」 という述語の定義が書かれています。

 definition let X,Y;
  pred X c= Y means
   x in X implies x in Y;
  reflexivity;
 end;

任意の$X,Y$に対して

$$X \subseteq Y$$

とは,任意の$x$について

$$x \in X \Rightarrow x \in Y$$

が成り立つことをいい,$reflexivity$は 任意の$X$に対してそれ自身

$$X \subseteq X$$

が成り立つことを表しています。