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

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