let Y be non empty TopStruct ; :: thesis: for X1, X2 being SubSpace of Y st the carrier of X1 c= the carrier of X2 holds
X1 is SubSpace of X2
let X1, X2 be SubSpace of Y; :: thesis: ( the carrier of X1 c= the carrier of X2 implies X1 is SubSpace of X2 )
set A1 = the carrier of X1;
set A2 = the carrier of X2;
A1: the carrier of X1 = [#] X1 ;
assume A2: the carrier of X1 c= the carrier of X2 ; :: thesis: X1 is SubSpace of X2
A3: the carrier of X2 = [#] X2 ;
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 ) )

proof

let P be Subset of X1; :: thesis: ( 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 ) )
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: ( ex Q being Subset of X2 st
( Q in the topology of X2 & P = Q /\ the carrier of X1 ) implies P in the topology of X1 )

proof

assume P in the topology of X1 ; :: thesis: ex Q being Subset of X2 st
( Q in the topology of X2 & P = Q /\ the carrier of X1 )
then consider R being Subset of Y such that
A4: R in the topology of Y 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: ( Q in the topology of X2 & P = Q /\ the carrier of X1 )
thus Q in the topology of X2 by A3, A4, PRE_TOPC:def 4; :: thesis: P = Q /\ the carrier of X1
Q /\ the carrier of X1 = R /\ ( the carrier of X2 /\ the carrier of X1) by XBOOLE_1:16
.= R /\ the carrier of X1 by A2, XBOOLE_1:28 ;
hence P = Q /\ the carrier of X1 by A5; :: thesis: verum

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: P in the topology of X1
consider R being Subset of Y such that
A8: R in the topology of Y 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 A2, XBOOLE_1:28 ;
hence P in the topology of X1 by A1, A8, PRE_TOPC:def 4; :: thesis: verum

end;

hence X1 is SubSpace of X2 by A1, A3, A2, PRE_TOPC:def 4; :: thesis: verum