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 :: thesis: ex Y being Subset-Family of X st
( Y c= FinMeetCl A & [#] TopStruct(# X,(UniCl (FinMeetCl A)) #) = union Y )
reconsider Y = {([#] TopStruct(# X,(UniCl (FinMeetCl A)) #))} as Subset-Family of X by ZFMISC_1:68;
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:31; :: thesis: [#] TopStruct(# X,(UniCl (FinMeetCl A)) #) = union Y
thus [#] TopStruct(# X,(UniCl (FinMeetCl A)) #) = union Y by ZFMISC_1:25; :: 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 b1 being Element of bool (bool the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #)) holds
( not b1 c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or union b1 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ) ) & ( for b1, b2 being Element of bool the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #) holds
( not b1 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or not b2 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or b1 /\ b2 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 b1, b2 being Element of bool the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #) holds
( not b1 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or not b2 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or b1 /\ b2 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 S1[ 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 S1[B] ) from SUBSET_1:sch 3();
 A4: 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 object ; :: thesis: ( x in a implies x in { (union B) where B is Subset of (FinMeetCl A) : B in b } )
assume A5: x in a ; :: thesis: x in { (union B) where B is Subset of (FinMeetCl A) : B in b }
then reconsider x9 = x as Subset of X ;
consider V being Subset-Family of X such that
A6: V c= FinMeetCl A and
A7: x9 = union V by A2, A5, Def1;
V in b by A3, A5, A6, A7;
hence x in { (union B) where B is Subset of (FinMeetCl A) : B in b } by A7; :: thesis: verum
end;
let x be object ; :: 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
A8: x = union B and
A9: B in b ;
ex c being Subset of TopStruct(# X,(UniCl (FinMeetCl A)) #) st
( c in a & c = union B ) by A3, A9;
hence x in a by A8; :: thesis: verum
end;
( union (union b) = union { (union B) where B is Subset of (FinMeetCl A) : B in b } & union b c= bool X ) by EQREL_1:54, XBOOLE_1:1;
hence union a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) by A4, 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
A10: F c= FinMeetCl A and
A11: 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
A12: G c= FinMeetCl A and
A13: b = union G by Def1;
A14: union (INTERSECTION (F,G)) = a /\ b by A11, A13, SETFAM_1:28;
A15: INTERSECTION (F,G) c= FinMeetCl A by A10, A12, Th13;
then INTERSECTION (F,G) is Subset-Family of X by XBOOLE_1:1;
hence a /\ b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) by A15, A14, Def1; :: thesis: verum