let X be non empty set ; :: thesis: for A being Subset-Family of X holds TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like
let A be Subset-Family of X; :: thesis: TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like
set T = TopStruct(# X,(UniCl (FinMeetCl A)) #);
A1: [#] TopStruct(# X,(UniCl (FinMeetCl A)) #) in FinMeetCl A by Th8;

now

reconsider Y = {([#] TopStruct(# X,(UniCl (FinMeetCl A)) #))} as Subset-Family of X by ZFMISC_1:80;
reconsider Y = Y as Subset-Family of X ;
take Y = Y; :: thesis: ( Y c= FinMeetCl A & [#] TopStruct(# X,(UniCl (FinMeetCl A)) #) = union Y )
thus Y c= FinMeetCl A by A1, ZFMISC_1:37; :: thesis: [#] TopStruct(# X,(UniCl (FinMeetCl A)) #) = union Y
thus [#] TopStruct(# X,(UniCl (FinMeetCl A)) #) = union Y by ZFMISC_1:31; :: thesis: verum

end;

hence the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #) in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) by Def1; :: according to PRE_TOPC:def 1 :: thesis: ( ( for b₁ being Element of bool (bool the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #)) holds
( not b₁ c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or union b₁ in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ) ) & ( for b₁, b₂ being Element of bool the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #) holds
( not b₁ in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or not b₂ in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or b₁ /\ b₂ in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ) ) )
thus for a being Subset-Family of TopStruct(# X,(UniCl (FinMeetCl A)) #) st a c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) holds
union a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) :: thesis: for b₁, b₂ being Element of bool the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #) holds
( not b₁ in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or not b₂ in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or b₁ /\ b₂ in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) )

proof

let a be Subset-Family of TopStruct(# X,(UniCl (FinMeetCl A)) #); :: thesis: ( a c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) implies union a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) )
assume A2: a c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ; :: thesis: union a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #)
defpred S₁[ set ] means ex c being Subset of TopStruct(# X,(UniCl (FinMeetCl A)) #) st
( c in a & c = union $1 );
consider b being Subset-Family of (FinMeetCl A) such that
A3: for B being Subset of (FinMeetCl A) holds
( B in b iff S₁[B] ) from SUBSET_1:sch 3();
A4: union (union b) = union { (union B) where B is Subset of (FinMeetCl A) : B in b } by BORSUK_1:17;
A5: a = { (union B) where B is Subset of (FinMeetCl A) : B in b }

proof

set gh = { (union B) where B is Subset of (FinMeetCl A) : B in b } ;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { (union B) where B is Subset of (FinMeetCl A) : B in b } c= a

let x be set ; :: thesis: ( x in a implies x in { (union B) where B is Subset of (FinMeetCl A) : B in b } )
assume A6: x in a ; :: thesis: x in { (union B) where B is Subset of (FinMeetCl A) : B in b }
then reconsider x' = x as Subset of X ;
consider V being Subset-Family of X such that
A7: V c= FinMeetCl A and
A8: x' = union V by A2, A6, Def1;
V in b by A3, A6, A7, A8;
hence x in { (union B) where B is Subset of (FinMeetCl A) : B in b } by A8; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (union B) where B is Subset of (FinMeetCl A) : B in b } or x in a )
assume x in { (union B) where B is Subset of (FinMeetCl A) : B in b } ; :: thesis: x in a
then consider B being Subset of (FinMeetCl A) such that
A9: x = union B and
A10: B in b ;
consider c being Subset of TopStruct(# X,(UniCl (FinMeetCl A)) #) such that
A11: c in a and
A12: c = union B by A3, A10;
thus x in a by A9, A11, A12; :: thesis: verum

end;

union b c= bool X by XBOOLE_1:1;
hence union a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) by A4, A5, Def1; :: thesis: verum

end;

let a, b be Subset of TopStruct(# X,(UniCl (FinMeetCl A)) #); :: thesis: ( not a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or not b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or a /\ b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) )
assume a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ; :: thesis: ( not b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or a /\ b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) )
then consider F being Subset-Family of X such that
A13: F c= FinMeetCl A and
A14: a = union F by Def1;
assume b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ; :: thesis: a /\ b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #)
then consider G being Subset-Family of X such that
A15: G c= FinMeetCl A and
A16: b = union G by Def1;
A17: INTERSECTION F,G c= FinMeetCl A by A13, A15, Th15;
then A18: INTERSECTION F,G is Subset-Family of X by XBOOLE_1:1;
union (INTERSECTION F,G) = a /\ b by A14, A16, SETFAM_1:39;
hence a /\ b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) by A17, A18, Def1; :: thesis: verum