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

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

hereby :: thesis:

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

proof

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

end;

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

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

end;

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

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 X, Yy2 being Subset of Y such that
A17: t = [:Xx1,Yy2:] and
A18: ex Y1 being Subset of XV st
( Y1 = Xx1 /\ ([#] XV) & Xx1 is open & Yy2 is open & [:Y1,Yy2:] in A ) ;
{t} c= bool the carrier of [:X,Y:]

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 [:X,Y:] by A17; :: thesis:

end;

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

proof

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

end;

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

end;

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

proof

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

end;

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

end;

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

proof

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

end;

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

proof

let s be object ; :: according to TARSKI:def 3 :: thesis:
assume A45: s in (union A) /\ oS ; :: thesis:
then s in union A by XBOOLE_0:def 4;
then consider A1 being set such that
A46: s in A1 and
A47: A1 in A by TARSKI:def 4;
s in oS by A45, XBOOLE_0:def 4;
then A48: s in A1 /\ oS by A46, XBOOLE_0:def 4;
reconsider A1 = A1 as Subset of [:X,Y:] by A47;
A1 /\ oS in AA by A47, TOPS_2:31;
hence s in union AA by A48, 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 A33, A34, A44;
then P9 is open by A36, BORSUK_1:5;
hence P in the topology of [:XV,Y:] by PRE_TOPC:def 2; :: thesis:

end;

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