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

set T = TopStruct(# D,t #);

TopStruct(# D,t #) is TopSpace-like

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

{ A where A is Subset of D : union A in the topology of X } c= bool D

proof

then reconsider t = { A where A is Subset of D : union A in the topology of X } as Subset-Family of D ;
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;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

set T = TopStruct(# D,t #);

TopStruct(# D,t #) is TopSpace-like

proof

then reconsider T = TopStruct(# D,t #) as strict TopSpace ;
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 b_{1} being Element of bool (bool the carrier of TopStruct(# D,t #)) holds

( not b_{1} c= the topology of TopStruct(# D,t #) or union b_{1} in the topology of TopStruct(# D,t #) ) ) & ( for b_{1}, b_{2} being Element of bool the carrier of TopStruct(# D,t #) holds

( not b_{1} in the topology of TopStruct(# D,t #) or not b_{2} in the topology of TopStruct(# D,t #) or b_{1} /\ b_{2} 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 b_{1}, b_{2} being Element of bool the carrier of TopStruct(# D,t #) holds

( not b_{1} in the topology of TopStruct(# D,t #) or not b_{2} in the topology of TopStruct(# D,t #) or b_{1} /\ b_{2} 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 ( 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 b

( not b

( not b

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 b

( not b

proof

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

{ (union A) where A is Subset of TopStruct(# D,t #) : A in a } c= the topology of X

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;A1: { (union A) where A is Subset of TopStruct(# D,t #) : A in a } c= bool the carrier of X

proof

assume A5:
a c= the topology of TopStruct(# D,t #)
; :: thesis: union a in the topology of TopStruct(# D,t #)
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

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

hence
e in bool the carrier of X
; :: thesis: verum
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;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

{ (union A) where A is Subset of TopStruct(# D,t #) : A in a } c= the topology of X

proof

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

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

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

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