set Y = TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #);
A1: for C, D being Subset of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #) st C in the topology of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #) & D in the topology of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #) holds
C /\ D in the topology of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #)

let C, D be Subset of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #); :: thesis:
assume that
A2: C in the topology of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #) and
A3: D in the topology of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #) ; :: thesis:
consider H1, G1 being Subset of X such that
A4: C = H1 \/ (G1 /\ A) and
A5: H1 in the topology of X and
A6: G1 in the topology of X by A2;
consider H2, G2 being Subset of X such that
A7: D = H2 \/ (G2 /\ A) and
A8: H2 in the topology of X and
A9: G2 in the topology of X by A3;
A10: C /\ D = (H1 /\ (H2 \/ (G2 /\ A))) \/ ((G1 /\ A) /\ (H2 \/ (G2 /\ A))) by A4, A7, XBOOLE_1:23
.= ((H1 /\ H2) \/ (H1 /\ (G2 /\ A))) \/ ((G1 /\ A) /\ (H2 \/ (G2 /\ A))) by XBOOLE_1:23
.= ((H1 /\ H2) \/ (H1 /\ (G2 /\ A))) \/ (((G1 /\ A) /\ H2) \/ ((G1 /\ A) /\ (G2 /\ A))) by XBOOLE_1:23
.= ((H1 /\ H2) \/ ((H1 /\ G2) /\ A)) \/ (((G1 /\ A) /\ H2) \/ ((G1 /\ A) /\ (G2 /\ A))) by XBOOLE_1:16
.= ((H1 /\ H2) \/ ((H1 /\ G2) /\ A)) \/ (((G1 /\ A) /\ H2) \/ (G1 /\ ((G2 /\ A) /\ A))) by XBOOLE_1:16
.= ((H1 /\ H2) \/ ((H1 /\ G2) /\ A)) \/ (((G1 /\ A) /\ H2) \/ (G1 /\ (G2 /\ (A /\ A)))) by XBOOLE_1:16
.= ((H1 /\ H2) \/ ((H1 /\ G2) /\ A)) \/ ((H2 /\ (G1 /\ A)) \/ ((G1 /\ G2) /\ A)) by XBOOLE_1:16
.= ((H1 /\ H2) \/ ((H1 /\ G2) /\ A)) \/ (((H2 /\ G1) /\ A) \/ ((G1 /\ G2) /\ A)) by XBOOLE_1:16
.= ((H1 /\ H2) \/ ((H1 /\ G2) /\ A)) \/ (((H2 /\ G1) \/ (G1 /\ G2)) /\ A) by XBOOLE_1:23
.= (H1 /\ H2) \/ (((H1 /\ G2) /\ A) \/ (((H2 /\ G1) \/ (G1 /\ G2)) /\ A)) by XBOOLE_1:4
.= (H1 /\ H2) \/ (((H1 /\ G2) \/ ((H2 /\ G1) \/ (G1 /\ G2))) /\ A) by XBOOLE_1:23
.= (H1 /\ H2) \/ ((((H1 /\ G2) \/ (H2 /\ G1)) \/ (G1 /\ G2)) /\ A) by XBOOLE_1:4 ;
G1 /\ G2 in the topology of X by A6, A9, PRE_TOPC:def 1;
then A11: G1 /\ G2 is open ;
A12: H2 /\ G1 is open by A6, A8, PRE_TOPC:def 1;
H1 /\ G2 in the topology of X by A5, A9, PRE_TOPC:def 1;
then H1 /\ G2 is open ;
then (H1 /\ G2) \/ (H2 /\ G1) is open by A12;
then ((H1 /\ G2) \/ (H2 /\ G1)) \/ (G1 /\ G2) is open by A11;
then A13: ((H1 /\ G2) \/ (H2 /\ G1)) \/ (G1 /\ G2) in the topology of X ;
H1 /\ H2 in the topology of X by A5, A8, PRE_TOPC:def 1;
hence C /\ D in the topology of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #) by A13, A10; :: thesis:

end;

A14: for FF being Subset-Family of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #) st FF c= the topology of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #) holds
union FF in the topology of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #)

proof

set SAA = { (G /\ A) where G is Subset of X : G in the topology of X } ;
{ (G /\ A) where G is Subset of X : G in the topology of X } c= A -extension_of_the_topology_of X by Th89;
then reconsider SAA = { (G /\ A) where G is Subset of X : G in the topology of X } as Subset-Family of X by TOPS_2:2;
let FF be Subset-Family of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #); :: thesis:
set AA = { (P \/ (S /\ A)) where P, S is Subset of X : ( P in the topology of X & S in the topology of X ) } ;
set FF1 = { H where H is Subset of X : ( H in the topology of X & ex G being Subset of X st
( G in the topology of X & H \/ (G /\ A) in FF ) ) } ;
set FF2 = { (G /\ A) where G is Subset of X : ( G in the topology of X & ex H being Subset of X st
( H in the topology of X & H \/ (G /\ A) in FF ) ) } ;

now :: thesis:

let W be object ; :: thesis:
assume W in { H where H is Subset of X : ( H in the topology of X & ex G being Subset of X st
( G in the topology of X & H \/ (G /\ A) in FF ) ) } ; :: thesis:
then ex H being Subset of X st
( W = H & H in the topology of X & ex G being Subset of X st
( G in the topology of X & H \/ (G /\ A) in FF ) ) ;
hence W in the topology of X ; :: thesis:

end;

then A15: { H where H is Subset of X : ( H in the topology of X & ex G being Subset of X st
( G in the topology of X & H \/ (G /\ A) in FF ) ) } c= the topology of X by TARSKI:def 3;

now :: thesis:

let W be object ; :: thesis:
assume W in { (G /\ A) where G is Subset of X : ( G in the topology of X & ex H being Subset of X st
( H in the topology of X & H \/ (G /\ A) in FF ) ) } ; :: thesis:
then ex G being Subset of X st
( W = G /\ A & G in the topology of X & ex H being Subset of X st
( H in the topology of X & H \/ (G /\ A) in FF ) ) ;
hence W in SAA ; :: thesis:

end;

then A16: { (G /\ A) where G is Subset of X : ( G in the topology of X & ex H being Subset of X st
( H in the topology of X & H \/ (G /\ A) in FF ) ) } c= SAA by TARSKI:def 3;
then reconsider FF2 = { (G /\ A) where G is Subset of X : ( G in the topology of X & ex H being Subset of X st
( H in the topology of X & H \/ (G /\ A) in FF ) ) } as Subset-Family of X by TOPS_2:2;
A17: union FF2 in SAA

proof

now :: thesis:

per cases ;

suppose A18: A = {} ; :: thesis:

now :: thesis:

let W be object ; :: thesis:
assume W in {{}} ; :: thesis:
then A19: W = {} /\ A by TARSKI:def 1;
{} in the topology of X by PRE_TOPC:1;
hence W in SAA by A19; :: thesis:

end;

then A20: {{}} c= SAA by TARSKI:def 3;

now :: thesis:

let W be object ; :: thesis:
assume W in SAA ; :: thesis:
then ex G being Subset of X st
( W = G /\ A & G in the topology of X ) ;
hence W in {{}} by A18, TARSKI:def 1; :: thesis:

end;

then SAA c= {{}} by TARSKI:def 3;
then A21: SAA = {{}} by A20;

now :: thesis:

per cases by A16, A21, ZFMISC_1:33;

suppose FF2 = {{}} ; :: thesis:

hence union FF2 = {} by ZFMISC_1:25; :: thesis:

end;

suppose FF2 = {} ; :: thesis:

hence union FF2 = {} by ZFMISC_1:2; :: thesis:

end;

hence union FF2 in SAA by A21, TARSKI:def 1; :: thesis:

end;

suppose A <> {} ; :: thesis:

then consider Y being non empty strict SubSpace of X such that
A22: A = the carrier of Y by TSEP_1:10;

now :: thesis:

let W be object ; :: thesis:
assume W in SAA ; :: thesis:
then consider G being Subset of X such that
A23: W = G /\ A and
A24: G in the topology of X ;
reconsider C = G /\ ([#] Y) as Subset of Y ;
C in the topology of Y by A24, PRE_TOPC:def 4;
hence W in the topology of Y by A22, A23; :: thesis:

end;

then A25: SAA c= the topology of Y by TARSKI:def 3;

A26: now :: thesis:

let W be object ; :: thesis:
assume A27: W in the topology of Y ; :: thesis:
then reconsider C = W as Subset of Y ;
ex G being Subset of X st
( G in the topology of X & C = G /\ ([#] Y) ) by A27, PRE_TOPC:def 4;
hence W in SAA by A22; :: thesis:

end;

then the topology of Y c= SAA by TARSKI:def 3;
then A28: the topology of Y = SAA by A25;
then reconsider SS = FF2 as Subset-Family of Y by A16, TOPS_2:2;
union SS in the topology of Y by A16, A28, PRE_TOPC:def 1;
hence union FF2 in SAA by A26; :: thesis:

end;

hence union FF2 in SAA ; :: thesis:

end;

reconsider FF1 = { H where H is Subset of X : ( H in the topology of X & ex G being Subset of X st
( G in the topology of X & H \/ (G /\ A) in FF ) ) } as Subset-Family of X by A15, TOPS_2:2;
A29: union FF1 in the topology of X by A15, PRE_TOPC:def 1;

now :: thesis:

let x be object ; :: thesis:
assume A30: x in (union FF1) \/ (union FF2) ; :: thesis:

now :: thesis:

per cases by A30, XBOOLE_0:def 3;

suppose x in union FF1 ; :: thesis:

then consider W being set such that
A31: x in W and
A32: W in FF1 by TARSKI:def 4;
consider H being Subset of X such that
A33: W = H and
H in the topology of X and
A34: ex G being Subset of X st
( G in the topology of X & H \/ (G /\ A) in FF ) by A32;
consider G being Subset of X such that
A35: H \/ (G /\ A) in FF by A34;
A36: H c= H \/ (G /\ A) by XBOOLE_1:7;
H \/ (G /\ A) c= union FF by A35, ZFMISC_1:74;
then H c= union FF by A36, XBOOLE_1:1;
hence x in union FF by A31, A33; :: thesis:

end;

suppose x in union FF2 ; :: thesis:

then consider W being set such that
A37: x in W and
A38: W in FF2 by TARSKI:def 4;
consider G being Subset of X such that
A39: W = G /\ A and
G in the topology of X and
A40: ex H being Subset of X st
( H in the topology of X & H \/ (G /\ A) in FF ) by A38;
consider H being Subset of X such that
A41: H \/ (G /\ A) in FF by A40;
A42: G /\ A c= H \/ (G /\ A) by XBOOLE_1:7;
H \/ (G /\ A) c= union FF by A41, ZFMISC_1:74;
then G /\ A c= union FF by A42, XBOOLE_1:1;
hence x in union FF by A37, A39; :: thesis:

end;

hence x in union FF ; :: thesis:

end;

then A43: (union FF1) \/ (union FF2) c= union FF by TARSKI:def 3;
assume A44: FF c= the topology of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #) ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
A45: union FF1 c= (union FF1) \/ (union FF2) by XBOOLE_1:7;
A46: union FF2 c= (union FF1) \/ (union FF2) by XBOOLE_1:7;
assume x in union FF ; :: thesis:
then consider W being set such that
A47: x in W and
A48: W in FF by TARSKI:def 4;
W in { (P \/ (S /\ A)) where P, S is Subset of X : ( P in the topology of X & S in the topology of X ) } by A44, A48;
then consider H, G being Subset of X such that
A49: W = H \/ (G /\ A) and
A50: ( H in the topology of X & G in the topology of X ) ;
G /\ A in FF2 by A48, A49, A50;
then G /\ A c= union FF2 by ZFMISC_1:74;
then A51: G /\ A c= (union FF1) \/ (union FF2) by A46, XBOOLE_1:1;
H in FF1 by A48, A49, A50;
then H c= union FF1 by ZFMISC_1:74;
then H c= (union FF1) \/ (union FF2) by A45, XBOOLE_1:1;
then H \/ (G /\ A) c= (union FF1) \/ (union FF2) by A51, XBOOLE_1:8;
hence x in (union FF1) \/ (union FF2) by A47, A49; :: thesis:

end;

then union FF c= (union FF1) \/ (union FF2) by TARSKI:def 3;
then union FF = (union FF1) \/ (union FF2) by A43;
hence union FF in the topology of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #) by A29, A17, Th90; :: thesis:

end;

( the topology of X c= A -extension_of_the_topology_of X & the carrier of X in the topology of X ) by Th88, PRE_TOPC:def 1;
hence TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #) is strict TopSpace by A14, A1, PRE_TOPC:def 1; :: thesis: