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 (FinMeetCl B) & TopStruct(# X,(UniCl B) #) 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 (FinMeetCl B) & TopStruct(# X,(UniCl B) #) 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 (FinMeetCl B) & TopStruct(# X,(UniCl B) #) is TopSpace-like )
thus UniCl B = UniCl (FinMeetCl B) :: thesis: TopStruct(# X,(UniCl B) #) is TopSpace-like

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: UniCl (FinMeetCl B) c= UniCl B

let x be object ; :: thesis: ( x in UniCl B implies x in UniCl (FinMeetCl B) )
assume A3: x in UniCl B ; :: thesis: x in UniCl (FinMeetCl B)
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 A3, CANTOR_1:def 1;
B c= FinMeetCl B by CANTOR_1:4;
then Y c= FinMeetCl B by A4;
hence x in UniCl (FinMeetCl B) by A5, CANTOR_1:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in UniCl (FinMeetCl B) or x in UniCl B )
assume A6: x in UniCl (FinMeetCl B) ; :: 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 A6, CANTOR_1:def 1;
FinMeetCl B c= UniCl B

proof

per cases ( B is empty or not B is empty ) ;

suppose B is empty ; :: thesis: FinMeetCl B c= UniCl B

hence FinMeetCl B c= UniCl B by A1, A2, Th1; :: thesis: verum

end;

suppose not B is empty ; :: thesis: FinMeetCl B c= UniCl B

hence FinMeetCl B c= UniCl B by A1, A2, Th2; :: thesis: verum

end;

end;

end;

then Y1 c= UniCl B by A7;
then union Y1 in UniCl (UniCl B) by CANTOR_1:def 1;
hence x in UniCl B by A8, YELLOW_9:15; :: thesis: verum

end;

hence TopStruct(# X,(UniCl B) #) is TopSpace-like by CANTOR_1:15; :: thesis: verum