let X, Y be set ; :: thesis: for A being Subset-Family of
for B being Subset-Family of holds
( ( A c= B implies UniCl A c= UniCl B ) & ( A = B implies UniCl A = UniCl B ) )
let A be Subset-Family of ; :: thesis: for B being Subset-Family of holds
( ( A c= B implies UniCl A c= UniCl B ) & ( A = B implies UniCl A = UniCl B ) )
let B be Subset-Family of ; :: thesis: ( ( A c= B implies UniCl A c= UniCl B ) & ( A = B implies UniCl A = UniCl B ) )

A1: now

let X, Y be set ; :: thesis: for A being Subset-Family of
for B being Subset-Family of st A c= B holds
UniCl A c= UniCl B
let A be Subset-Family of ; :: thesis: for B being Subset-Family of st A c= B holds
UniCl A c= UniCl B
let B be Subset-Family of ; :: thesis: ( A c= B implies UniCl A c= UniCl B )
assume A2: A c= B ; :: thesis: UniCl A c= UniCl B
thus UniCl A c= UniCl B :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in UniCl A or x in UniCl B )
assume x in UniCl A ; :: thesis: x in UniCl B
then consider y being Subset-Family of such that
A3: y c= A and
A4: x = union y by CANTOR_1:def 1;
y c= B by A2, A3, XBOOLE_1:1;
then y is Subset-Family of by XBOOLE_1:1;
then ex y being Subset-Family of st
( y c= B & x = union y ) by A2, A3, A4, XBOOLE_1:1;
hence x in UniCl B by CANTOR_1:def 1; :: thesis: verum

end;

end;

hence ( A c= B implies UniCl A c= UniCl B ) ; :: thesis: ( A = B implies UniCl A = UniCl B )
assume A = B ; :: thesis: UniCl A = UniCl B
hence ( UniCl A c= UniCl B & UniCl B c= UniCl A ) by A1; :: according to XBOOLE_0:def 10 :: thesis: verum