let X be non empty set ; :: thesis: for B, Y being Subset-Family of X st Y c= UniCl B holds
union Y in UniCl B
let B, Y be Subset-Family of X; :: thesis: ( Y c= UniCl B implies union Y in UniCl B )
assume Y c= UniCl B ; :: thesis: union Y in UniCl B
then union Y in UniCl (UniCl B) by CANTOR_1:def 1;
hence union Y in UniCl B by YELLOW_9:15; :: thesis: verum