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

union FF in the topology of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #)

hence TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #) is strict TopSpace by A14, A1, PRE_TOPC:def 1; :: thesis: verum

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

proof

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
let C, D be Subset of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #); :: thesis: ( 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) #) implies C /\ D in the topology of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #) )

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: C /\ D in the topology of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #)

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: verum

end;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: C /\ D in the topology of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #)

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: verum

union FF in the topology of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #)

proof

( 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;
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: ( FF c= the topology of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #) implies union FF in the topology of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #) )

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

( G in the topology of X & H \/ (G /\ A) in FF ) ) } c= the topology of X by TARSKI:def 3;

( 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

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

assume A44: FF c= the topology of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #) ; :: thesis: union FF in the topology of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #)

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: verum

end;{ (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: ( FF c= the topology of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #) implies union FF in the topology of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #) )

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: for W being object st 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 ) ) } holds

W in the topology of X

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 ) ) } holds

W in the topology of X

let W be object ; :: thesis: ( 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 ) ) } implies W in the topology of X )

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: W in the topology of X

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: verum

end;( G in the topology of X & H \/ (G /\ A) in FF ) ) } implies W in the topology of X )

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: W in the topology of X

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: verum

( G in the topology of X & H \/ (G /\ A) in FF ) ) } c= the topology of X by TARSKI:def 3;

now :: thesis: for W being object st 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 ) ) } holds

W in SAA

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 ) ) } holds

W in SAA

let W be object ; :: thesis: ( 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 ) ) } implies W in SAA )

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: W in SAA

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: verum

end;( H in the topology of X & H \/ (G /\ A) in FF ) ) } implies W in SAA )

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: W in SAA

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: verum

( 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

end;

reconsider FF1 = { H where H is Subset of X : ( H in the topology of X & ex G being Subset of X st now :: thesis: union FF2 in SAAend;

hence
union FF2 in SAA
; :: thesis: verumper cases
( A = {} or A <> {} )
;

end;

suppose A18:
A = {}
; :: thesis: union FF2 in SAA

then A21: SAA = {{}} by A20;

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

end;

now :: thesis: for W being object st W in {{}} holds

W in SAA

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

let W be object ; :: thesis: ( W in {{}} implies W in SAA )

assume W in {{}} ; :: thesis: W in SAA

then A19: W = {} /\ A by TARSKI:def 1;

{} in the topology of X by PRE_TOPC:1;

hence W in SAA by A19; :: thesis: verum

end;assume W in {{}} ; :: thesis: W in SAA

then A19: W = {} /\ A by TARSKI:def 1;

{} in the topology of X by PRE_TOPC:1;

hence W in SAA by A19; :: thesis: verum

now :: thesis: for W being object st W in SAA holds

W in {{}}

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

let W be object ; :: thesis: ( W in SAA implies W in {{}} )

assume W in SAA ; :: thesis: W in {{}}

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: verum

end;assume W in SAA ; :: thesis: W in {{}}

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: verum

then A21: SAA = {{}} by A20;

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

suppose
A <> {}
; :: thesis: union FF2 in SAA

then consider Y being non empty strict SubSpace of X such that

A22: A = the carrier of Y by TSEP_1:10;

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: verum

end;A22: A = the carrier of Y by TSEP_1:10;

now :: thesis: for W being object st W in SAA holds

W in the topology of Y

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

let W be object ; :: thesis: ( W in SAA implies W in the topology of Y )

assume W in SAA ; :: thesis: W in the topology of Y

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: verum

end;assume W in SAA ; :: thesis: W in the topology of Y

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: verum

A26: now :: thesis: for W being object st W in the topology of Y holds

W in SAA

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

let W be object ; :: thesis: ( W in the topology of Y implies W in SAA )

assume A27: W in the topology of Y ; :: thesis: W in SAA

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: verum

end;assume A27: W in the topology of Y ; :: thesis: W in SAA

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: verum

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: verum

( 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: for x being object st x in (union FF1) \/ (union FF2) holds

x in union FF

then A43:
(union FF1) \/ (union FF2) c= union FF
by TARSKI:def 3;x in union FF

let x be object ; :: thesis: ( x in (union FF1) \/ (union FF2) implies x in union FF )

assume A30: x in (union FF1) \/ (union FF2) ; :: thesis: x in union FF

end;assume A30: x in (union FF1) \/ (union FF2) ; :: thesis: x in union FF

now :: thesis: x in union FFend;

hence
x in union FF
; :: thesis: verumper cases
( x in union FF1 or x in union FF2 )
by A30, XBOOLE_0:def 3;

end;

suppose
x in union FF1
; :: thesis: x in union FF

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: verum

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

suppose
x in union FF2
; :: thesis: x in union FF

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: verum

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

assume A44: FF c= the topology of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #) ; :: thesis: union FF in the topology of TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #)

now :: thesis: for x being object st x in union FF holds

x in (union FF1) \/ (union FF2)

then
union FF c= (union FF1) \/ (union FF2)
by TARSKI:def 3;x in (union FF1) \/ (union FF2)

let x be object ; :: thesis: ( x in union FF implies x in (union FF1) \/ (union FF2) )

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: x in (union FF1) \/ (union FF2)

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: verum

end;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: x in (union FF1) \/ (union FF2)

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: verum

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: verum

hence TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #) is strict TopSpace by A14, A1, PRE_TOPC:def 1; :: thesis: verum