集合の合弁の定義

任意の集合族(集合の集合)$X$に対して,$X$に属する 集合の全ての合弁が,$X$から$\cup X$をつくる$functor$(作用)として定義されています。

 definition let X;
   func union X means
    x in it iff ex Y st x in Y & Y in X;
  correctness;
 end;

任意の$X$に対して,$functor$(作用)$\cup X$とは,$X$に,

任意の$x$に対して

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

となる集合を対応させる作用であること表しています 。