set t = { A where A is Subset of D : union A in the topology of X } ;
{ A where A is Subset of D : union A in the topology of X } c= bool D
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { A where A is Subset of D : union A in the topology of X } or e in bool D )
assume e in { A where A is Subset of D : union A in the topology of X } ; :: thesis: e in bool D
then ex A being Subset of D st
( e = A & union A in the topology of X ) ;
hence e in bool D ; :: thesis: verum
end;
then reconsider t = { A where A is Subset of D : union A in the topology of X } as Subset-Family of D ;
set T = TopStruct(# D,t #);
TopStruct(# D,t #) is TopSpace-like
proof
union D = the carrier of X by EQREL_1:def 4;
then ( D c= D & union D in the topology of X ) by PRE_TOPC:def 1;
hence the carrier of TopStruct(# D,t #) in the topology of TopStruct(# D,t #) ; :: according to PRE_TOPC:def 1 :: thesis: ( ( for b1 being Element of bool (bool the carrier of TopStruct(# D,t #)) holds
( not b1 c= the topology of TopStruct(# D,t #) or union b1 in the topology of TopStruct(# D,t #) ) ) & ( for b1, b2 being Element of bool the carrier of TopStruct(# D,t #) holds
( not b1 in the topology of TopStruct(# D,t #) or not b2 in the topology of TopStruct(# D,t #) or b1 /\ b2 in the topology of TopStruct(# D,t #) ) ) )
thus for a being Subset-Family of TopStruct(# D,t #) st a c= the topology of TopStruct(# D,t #) holds
union a in the topology of TopStruct(# D,t #) :: thesis: for b1, b2 being Element of bool the carrier of TopStruct(# D,t #) holds
( not b1 in the topology of TopStruct(# D,t #) or not b2 in the topology of TopStruct(# D,t #) or b1 /\ b2 in the topology of TopStruct(# D,t #) )
proof
let a be Subset-Family of TopStruct(# D,t #); :: thesis: ( a c= the topology of TopStruct(# D,t #) implies union a in the topology of TopStruct(# D,t #) )
A1: { (union A) where A is Subset of TopStruct(# D,t #) : A in a } c= bool the carrier of X
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (union A) where A is Subset of TopStruct(# D,t #) : A in a } or e in bool the carrier of X )
reconsider ee = e as set by TARSKI:1;
assume e in { (union A) where A is Subset of TopStruct(# D,t #) : A in a } ; :: thesis: e in bool the carrier of X
then consider A being Subset of TopStruct(# D,t #) such that
A2: e = union A and
A in a ;
ee c= the carrier of X
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in ee or u in the carrier of X )
assume u in ee ; :: thesis: u in the carrier of X
then consider x being set such that
A3: u in x and
A4: x in A by A2, TARSKI:def 4;
x in the carrier of TopStruct(# D,t #) by A4;
hence u in the carrier of X by A3; :: thesis: verum
end;
hence e in bool the carrier of X ; :: thesis: verum
end;
assume A5: a c= the topology of TopStruct(# D,t #) ; :: thesis: union a in the topology of TopStruct(# D,t #)
{ (union A) where A is Subset of TopStruct(# D,t #) : A in a } c= the topology of X
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (union A) where A is Subset of TopStruct(# D,t #) : A in a } or e in the topology of X )
assume e in { (union A) where A is Subset of TopStruct(# D,t #) : A in a } ; :: thesis: e in the topology of X
then consider A being Subset of TopStruct(# D,t #) such that
A6: e = union A and
A7: A in a ;
A in the topology of TopStruct(# D,t #) by A5, A7;
then ex B being Subset of D st
( A = B & union B in the topology of X ) ;
hence e in the topology of X by A6; :: thesis: verum
end;
then union { (union A) where A is Subset of TopStruct(# D,t #) : A in a } in the topology of X by A1, PRE_TOPC:def 1;
then union (union a) in the topology of X by EQREL_1:54;
hence union a in the topology of TopStruct(# D,t #) ; :: thesis: verum
end;
let a, b be Subset of TopStruct(# D,t #); :: thesis: ( not a in the topology of TopStruct(# D,t #) or not b in the topology of TopStruct(# D,t #) or a /\ b in the topology of TopStruct(# D,t #) )
assume that
A8: a in the topology of TopStruct(# D,t #) and
A9: b in the topology of TopStruct(# D,t #) ; :: thesis: a /\ b in the topology of TopStruct(# D,t #)
consider B being Subset of D such that
A10: b = B and
A11: union B in the topology of X by A9;
consider A being Subset of D such that
A12: a = A and
A13: union A in the topology of X by A8;
union (A /\ B) = (union A) /\ (union B) by EQREL_1:62;
then union (A /\ B) in the topology of X by A13, A11, PRE_TOPC:def 1;
hence a /\ b in the topology of TopStruct(# D,t #) by A12, A10; :: thesis: verum
end;
then reconsider T = TopStruct(# D,t #) as strict TopSpace ;
take T ; :: thesis: ( the carrier of T = D & the topology of T = { A where A is Subset of D : union A in the topology of X } )
thus ( the carrier of T = D & the topology of T = { A where A is Subset of D : union A in the topology of X } ) ; :: thesis: verum