set Y = TopStruct(# the carrier of X, #);
A1: for C, D being Subset of TopStruct(# the carrier of X, #) st C in the topology of TopStruct(# the carrier of X, #) & D in the topology of TopStruct(# the carrier of X, #) holds
C /\ D in the topology of TopStruct(# the carrier of X, #)
proof
let C, D be Subset of TopStruct(# the carrier of X, #); :: thesis: ( C in the topology of TopStruct(# the carrier of X, #) & D in the topology of TopStruct(# the carrier of X, #) implies C /\ D in the topology of TopStruct(# the carrier of X, #) )
assume that
A2: C in the topology of TopStruct(# the carrier of X, #) and
A3: D in the topology of TopStruct(# the carrier of X, #) ; :: thesis: C /\ D in the topology of TopStruct(# the carrier 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
.= ((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 ;
then A11: G1 /\ G2 is open ;
A12: H2 /\ G1 is open by ;
H1 /\ G2 in the topology of X by ;
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 ;
hence C /\ D in the topology of TopStruct(# the carrier of X, #) by ; :: thesis: verum
end;
A14: for FF being Subset-Family of TopStruct(# the carrier of X, #) st FF c= the topology of TopStruct(# the carrier of X, #) holds
union FF in the topology of TopStruct(# the carrier 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, #); :: thesis: ( FF c= the topology of TopStruct(# the carrier of X, #) implies union FF in the topology of TopStruct(# the carrier 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
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;
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: 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
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;
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: union FF2 in SAA
per cases ( A = {} or A <> {} ) ;
suppose A18: A = {} ; :: thesis: union FF2 in SAA
now :: thesis: for W being object st W in holds
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;
then A20: {{}} c= SAA by TARSKI:def 3;
now :: thesis: for W being object st W in SAA holds
W in
let W be object ; :: thesis: ( W in SAA implies W in )
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 ; :: thesis: verum
end;
then SAA c= by TARSKI:def 3;
then A21: SAA = by A20;
hence union FF2 in SAA by ; :: thesis: verum
end;
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;
now :: thesis: for W being object st W in SAA holds
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 ;
hence W in the topology of Y by ; :: thesis: verum
end;
then A25: SAA c= the topology of Y by TARSKI:def 3;
A26: now :: thesis: for W being object st W in the topology of Y holds
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 ;
hence W in SAA by A22; :: thesis: verum
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 ;
union SS in the topology of Y by ;
hence union FF2 in SAA by A26; :: thesis: verum
end;
end;
end;
hence union FF2 in SAA ; :: thesis: verum
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 ;
A29: union FF1 in the topology of X by ;
now :: thesis: for x being object st x in (union FF1) \/ (union FF2) holds
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
now :: thesis: x in union FF
per cases ( x in union FF1 or x in union FF2 ) by ;
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 ;
then H c= union FF by ;
hence x in union FF by ; :: thesis: verum
end;
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 ;
then G /\ A c= union FF by ;
hence x in union FF by ; :: thesis: verum
end;
end;
end;
hence x in union FF ; :: thesis: verum
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, #) ; :: thesis: union FF in the topology of TopStruct(# the carrier of X, #)
now :: thesis: for x being object st x in union FF holds
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 ;
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 ;
then G /\ A c= union FF2 by ZFMISC_1:74;
then A51: G /\ A c= (union FF1) \/ (union FF2) by ;
H in FF1 by ;
then H c= union FF1 by ZFMISC_1:74;
then H c= (union FF1) \/ (union FF2) by ;
then H \/ (G /\ A) c= (union FF1) \/ (union FF2) by ;
hence x in (union FF1) \/ (union FF2) by ; :: thesis: verum
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, #) by ; :: thesis: verum
end;
( the topology of X c= A -extension_of_the_topology_of X & the carrier of X in the topology of X ) by ;
hence TopStruct(# the carrier of X, #) is strict TopSpace by ; :: thesis: verum