:: deftheorem Def1 defines UniCl CANTOR_1:def 1 :
for X being set
for A, b₃ being Subset-Family of X holds
( b₃ = UniCl A iff for x being Subset of X holds
( x in b₃ iff ex Y being Subset-Family of X st
( Y c= A & x = union Y ) ) );