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

( 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

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 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: verumhereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: UniCl (FinMeetCl B) c= UniCl B

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

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 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