let X, Y be TopSpace; :: thesis:
let XV be SubSpace of X; :: thesis:
set S = [:Y,XV:];
set T = [:Y,X:];
A1: the carrier of [:Y,XV:] = [: the carrier of Y, the carrier of XV:] by BORSUK_1:def 2;
A2: ( the carrier of [:Y,X:] = [: the carrier of Y, the carrier of X:] & the carrier of XV c= the carrier of X ) by BORSUK_1:1, BORSUK_1:def 2;
A3: for P being Subset of [:Y,XV:] holds
( P in the topology of [:Y,XV:] iff ex Q being Subset of [:Y,X:] st
( Q in the topology of [:Y,X:] & P = Q /\ ([#] [:Y,XV:]) ) )

reconsider oS = [#] [:Y,XV:] as Subset of [:Y,X:] by A1, A2, ZFMISC_1:96;
let P be Subset of [:Y,XV:]; :: thesis:
reconsider P9 = P as Subset of [:Y,XV:] ;

hereby :: thesis:

assume P in the topology of [:Y,XV:] ; :: thesis:
then P9 is open by PRE_TOPC:def 2;
then consider A being Subset-Family of [:Y,XV:] such that
A4: P9 = union A and
A5: for e being set st e in A holds
ex X1 being Subset of Y ex Y1 being Subset of XV st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5;
set AA = { [:X1,Y2:] where X1 is Subset of Y, Y2 is Subset of X : ex Y1 being Subset of XV st
( Y1 = Y2 /\ ([#] XV) & X1 is open & Y2 is open & [:X1,Y1:] in A ) } ;
{ [:X1,Y2:] where X1 is Subset of Y, Y2 is Subset of X : ex Y1 being Subset of XV st
( Y1 = Y2 /\ ([#] XV) & X1 is open & Y2 is open & [:X1,Y1:] in A ) } c= bool the carrier of [:Y,X:]

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in { [:X1,Y2:] where X1 is Subset of Y, Y2 is Subset of X : ex Y1 being Subset of XV st
( Y1 = Y2 /\ ([#] XV) & X1 is open & Y2 is open & [:X1,Y1:] in A ) } ; :: thesis:
then ex Xx1 being Subset of Y ex Yy2 being Subset of X st
( a = [:Xx1,Yy2:] & ex Y1 being Subset of XV st
( Y1 = Yy2 /\ ([#] XV) & Xx1 is open & Yy2 is open & [:Xx1,Y1:] in A ) ) ;
hence a in bool the carrier of [:Y,X:] ; :: thesis:

end;

then reconsider AA = { [:X1,Y2:] where X1 is Subset of Y, Y2 is Subset of X : ex Y1 being Subset of XV st
( Y1 = Y2 /\ ([#] XV) & X1 is open & Y2 is open & [:X1,Y1:] in A ) } as Subset-Family of [:Y,X:] ;
reconsider AA = AA as Subset-Family of [:Y,X:] ;
A6: P c= (union AA) /\ ([#] [:Y,XV:])

proof

let p be object ; :: according to TARSKI:def 3 :: thesis:
assume p in P ; :: thesis:
then consider A1 being set such that
A7: p in A1 and
A8: A1 in A by A4, TARSKI:def 4;
reconsider A1 = A1 as Subset of [:Y,XV:] by A8;
consider X2 being Subset of Y, Y2 being Subset of XV such that
A9: A1 = [:X2,Y2:] and
A10: X2 is open and
A11: Y2 is open by A5, A8;
Y2 in the topology of XV by A11, PRE_TOPC:def 2;
then consider Q1 being Subset of X such that
A12: Q1 in the topology of X and
A13: Y2 = Q1 /\ ([#] XV) by PRE_TOPC:def 4;
consider p1, p2 being object such that
A14: p1 in X2 and
A15: p2 in Y2 and
A16: p = [p1,p2] by A7, A9, ZFMISC_1:def 2;
reconsider Q1 = Q1 as Subset of X ;
set EX = [:X2,Q1:];
p2 in Q1 by A15, A13, XBOOLE_0:def 4;
then A17: p in [:X2,Q1:] by A14, A16, ZFMISC_1:87;
Q1 is open by A12, PRE_TOPC:def 2;
then [:X2,Q1:] in { [:Xx1,Yy2:] where Xx1 is Subset of Y, Yy2 is Subset of X : ex Z1 being Subset of XV st
( Z1 = Yy2 /\ ([#] XV) & Xx1 is open & Yy2 is open & [:Xx1,Z1:] in A ) } by A8, A9, A10, A13;
then p in union AA by A17, TARSKI:def 4;
hence p in (union AA) /\ ([#] [:Y,XV:]) by A7, A8, XBOOLE_0:def 4; :: thesis:

end;

AA c= the topology of [:Y,X:]

proof

let t be object ; :: according to TARSKI:def 3 :: thesis:
set A9 = {t};
assume t in AA ; :: thesis:
then consider Xx1 being Subset of Y, Yy2 being Subset of X such that
A18: t = [:Xx1,Yy2:] and
A19: ex Y1 being Subset of XV st
( Y1 = Yy2 /\ ([#] XV) & Xx1 is open & Yy2 is open & [:Xx1,Y1:] in A ) ;
{t} c= bool the carrier of [:Y,X:]

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in {t} ; :: thesis:
then a = t by TARSKI:def 1;
hence a in bool the carrier of [:Y,X:] by A18; :: thesis:

end;

then reconsider A9 = {t} as Subset-Family of [:Y,X:] ;
A20: A9 c= { [:X1,Y1:] where X1 is Subset of Y, Y1 is Subset of X : ( X1 in the topology of Y & Y1 in the topology of X ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in A9 ; :: thesis:
then A21: x = [:Xx1,Yy2:] by A18, TARSKI:def 1;
( Xx1 in the topology of Y & Yy2 in the topology of X ) by A19, PRE_TOPC:def 2;
hence x in { [:X1,Y1:] where X1 is Subset of Y, Y1 is Subset of X : ( X1 in the topology of Y & Y1 in the topology of X ) } by A21; :: thesis:

end;

t = union A9 ;
then t in { (union As) where As is Subset-Family of [:Y,X:] : As c= { [:X1,Y1:] where X1 is Subset of Y, Y1 is Subset of X : ( X1 in the topology of Y & Y1 in the topology of X ) } } by A20;
hence t in the topology of [:Y,X:] by BORSUK_1:def 2; :: thesis:

end;

then A22: union AA in the topology of [:Y,X:] by PRE_TOPC:def 1;
(union AA) /\ ([#] [:Y,XV:]) c= P

proof

let h be object ; :: according to TARSKI:def 3 :: thesis:
assume A23: h in (union AA) /\ ([#] [:Y,XV:]) ; :: thesis:
then h in union AA by XBOOLE_0:def 4;
then consider A2 being set such that
A24: h in A2 and
A25: A2 in AA by TARSKI:def 4;
consider Xx1 being Subset of Y, Yy2 being Subset of X such that
A26: A2 = [:Xx1,Yy2:] and
A27: ex Y1 being Subset of XV st
( Y1 = Yy2 /\ ([#] XV) & Xx1 is open & Yy2 is open & [:Xx1,Y1:] in A ) by A25;
consider Yy1 being Subset of XV such that
A28: Yy1 = Yy2 /\ ([#] XV) and
Xx1 is open and
Yy2 is open and
A29: [:Xx1,Yy1:] in A by A27;
consider p1, p2 being object such that
A30: p1 in Xx1 and
A31: p2 in Yy2 and
A32: h = [p1,p2] by A24, A26, ZFMISC_1:def 2;
p2 in the carrier of XV by A1, A23, A32, ZFMISC_1:87;
then p2 in Yy2 /\ ([#] XV) by A31, XBOOLE_0:def 4;
then h in [:Xx1,Yy1:] by A30, A32, A28, ZFMISC_1:87;
hence h in P by A4, A29, TARSKI:def 4; :: thesis:

end;

then P = (union AA) /\ ([#] [:Y,XV:]) by A6;
hence ex Q being Subset of [:Y,X:] st
( Q in the topology of [:Y,X:] & P = Q /\ ([#] [:Y,XV:]) ) by A22; :: thesis:

end;

given Q being Subset of [:Y,X:] such that A33: Q in the topology of [:Y,X:] and
A34: P = Q /\ ([#] [:Y,XV:]) ; :: thesis:
reconsider Q9 = Q as Subset of [:Y,X:] ;
Q9 is open by A33, PRE_TOPC:def 2;
then consider A being Subset-Family of [:Y,X:] such that
A35: Q9 = union A and
A36: for e being set st e in A holds
ex X1 being Subset of Y ex Y1 being Subset of X st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5;
reconsider A = A as Subset-Family of [:Y,X:] ;
reconsider AA = A | oS as Subset-Family of ([:Y,X:] | oS) ;
reconsider AA = AA as Subset-Family of [:Y,XV:] by PRE_TOPC:8;
reconsider AA = AA as Subset-Family of [:Y,XV:] ;
A37: for e being set st e in AA holds
ex X1 being Subset of Y ex Y1 being Subset of XV st
( e = [:X1,Y1:] & X1 is open & Y1 is open )

proof

let e be set ; :: thesis:
assume A38: e in AA ; :: thesis:
then reconsider e9 = e as Subset of ([:Y,X:] | oS) ;
consider R being Subset of [:Y,X:] such that
A39: R in A and
A40: R /\ oS = e9 by A38, TOPS_2:def 3;
consider X1 being Subset of Y, Y1 being Subset of X such that
A41: R = [:X1,Y1:] and
A42: X1 is open and
A43: Y1 is open by A36, A39;
reconsider D2 = Y1 /\ ([#] XV) as Subset of XV ;
Y1 in the topology of X by A43, PRE_TOPC:def 2;
then D2 in the topology of XV by PRE_TOPC:def 4;
then A44: D2 is open by PRE_TOPC:def 2;
[#] [:Y,XV:] = [:([#] Y),([#] XV):] by BORSUK_1:def 2;
then e9 = [:(X1 /\ ([#] Y)),(Y1 /\ ([#] XV)):] by A40, A41, ZFMISC_1:100;
hence ex X1 being Subset of Y ex Y1 being Subset of XV st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by A42, A44; :: thesis:

end;

A45: (union A) /\ oS c= union AA

proof

let s be object ; :: according to TARSKI:def 3 :: thesis:
assume A46: s in (union A) /\ oS ; :: thesis:
then s in union A by XBOOLE_0:def 4;
then consider A1 being set such that
A47: s in A1 and
A48: A1 in A by TARSKI:def 4;
s in oS by A46, XBOOLE_0:def 4;
then A49: s in A1 /\ oS by A47, XBOOLE_0:def 4;
reconsider A1 = A1 as Subset of [:Y,X:] by A48;
A1 /\ oS in AA by A48, TOPS_2:31;
hence s in union AA by A49, TARSKI:def 4; :: thesis:

end;

union AA c= union A by TOPS_2:34;
then union AA c= (union A) /\ oS by XBOOLE_1:19;
then P = union AA by A34, A35, A45;
then P9 is open by A37, BORSUK_1:5;
hence P in the topology of [:Y,XV:] by PRE_TOPC:def 2; :: thesis:

end;

[#] [:Y,XV:] c= [#] [:Y,X:] by A1, A2, ZFMISC_1:96;
hence [:Y,XV:] is SubSpace of [:Y,X:] by A3, PRE_TOPC:def 4; :: thesis: