let X be non empty set ; :: thesis: for B being Subset-Family of X st ( for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB ) & X = union B holds
( UniCl B = UniCl () & TopStruct(# X,() #) is TopSpace-like )

let B be Subset-Family of X; :: thesis: ( ( for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB ) & X = union B implies ( UniCl B = UniCl () & TopStruct(# X,() #) is TopSpace-like ) )
assume that
A1: for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB and
A2: X = union B ; :: thesis: ( UniCl B = UniCl () & TopStruct(# X,() #) is TopSpace-like )
thus UniCl B = UniCl () :: thesis: TopStruct(# X,() #) is TopSpace-like
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis:
let x be object ; :: thesis: ( x in UniCl B implies x in UniCl () )
assume A3: x in UniCl B ; :: thesis: x in UniCl ()
then reconsider x0 = x as Subset of X ;
consider Y being Subset-Family of X such that
A4: Y c= B and
A5: x = union Y by ;
B c= FinMeetCl B by CANTOR_1:4;
then Y c= FinMeetCl B by A4;
hence x in UniCl () by ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in UniCl () or x in UniCl B )
assume A6: x in UniCl () ; :: thesis: x in UniCl B
then reconsider x0 = x as Subset of X ;
consider Y1 being Subset-Family of X such that
A7: Y1 c= FinMeetCl B and
A8: x = union Y1 by ;
FinMeetCl B c= UniCl B
proof end;
then Y1 c= UniCl B by A7;
then union Y1 in UniCl () by CANTOR_1:def 1;
hence x in UniCl B by ; :: thesis: verum
end;
hence TopStruct(# X,() #) is TopSpace-like by CANTOR_1:15; :: thesis: verum