let X be TopSpace; :: thesis:
let X1, X2 be SubSpace of X; :: thesis:
set A1 = the carrier of X1;
set A2 = the carrier of X2;
A1: the carrier of X1 = [#] X1 ;
A2: the carrier of X2 = [#] X2 ;
thus ( the carrier of X1 c= the carrier of X2 implies X1 is SubSpace of X2 ) :: thesis:

assume A3: the carrier of X1 c= the carrier of X2 ; :: thesis:
for P being Subset of X1 holds
( P in the topology of X1 iff ex Q being Subset of X2 st
( Q in the topology of X2 & P = Q /\ the carrier of X1 ) )

let P be Subset of X1; :: thesis:
thus ( P in the topology of X1 implies ex Q being Subset of X2 st
( Q in the topology of X2 & P = Q /\ the carrier of X1 ) ) :: thesis:

assume P in the topology of X1 ; :: thesis:
then consider R being Subset of X such that
A4: R in the topology of X and
A5: P = R /\ the carrier of X1 by A1, PRE_TOPC:def 4;
reconsider Q = R /\ the carrier of X2 as Subset of X2 by XBOOLE_1:17;
take Q ; :: thesis:
thus Q in the topology of X2 by A2, A4, PRE_TOPC:def 4; :: thesis:
Q /\ the carrier of X1 = R /\ ( the carrier of X2 /\ the carrier of X1) by XBOOLE_1:16
.= R /\ the carrier of X1 by A3, XBOOLE_1:28 ;
hence P = Q /\ the carrier of X1 by A5; :: thesis:

end;

given Q being Subset of X2 such that A6: Q in the topology of X2 and
A7: P = Q /\ the carrier of X1 ; :: thesis:
consider R being Subset of X such that
A8: R in the topology of X and
A9: Q = R /\ ([#] X2) by A6, PRE_TOPC:def 4;
P = R /\ ( the carrier of X2 /\ the carrier of X1) by A7, A9, XBOOLE_1:16
.= R /\ the carrier of X1 by A3, XBOOLE_1:28 ;
hence P in the topology of X1 by A1, A8, PRE_TOPC:def 4; :: thesis:

end;

end;