let X, Y be set ; :: thesis: for A being Subset-Family of X
for B being Subset-Family of Y holds
( ( A c= B implies UniCl A c= UniCl B ) & ( A = B implies UniCl A = UniCl B ) )
let A be Subset-Family of X; :: thesis: for B being Subset-Family of Y holds
( ( A c= B implies UniCl A c= UniCl B ) & ( A = B implies UniCl A = UniCl B ) )
let B be Subset-Family of Y; :: thesis: ( ( A c= B implies UniCl A c= UniCl B ) & ( A = B implies UniCl A = UniCl B ) )
A1: now :: thesis: for X, Y being set
for A being Subset-Family of X
for B being Subset-Family of Y st A c= B holds
UniCl A c= UniCl B
let X, Y be set ; :: thesis: for A being Subset-Family of X
for B being Subset-Family of Y st A c= B holds
UniCl A c= UniCl B
let A be Subset-Family of X; :: thesis: for B being Subset-Family of Y st A c= B holds
UniCl A c= UniCl B
let B be Subset-Family of Y; :: 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 object ; :: 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 X such that
A3: y c= A and
A4: x = union y by CANTOR_1:def 1;
y c= B by A2, A3;
then y is Subset-Family of Y by XBOOLE_1:1;
then ex y being Subset-Family of Y 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