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 ;
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 ; :: 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 ;
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 ;
P = R /\ ( the carrier of X2 /\ the carrier of X1) by
.= R /\ the carrier of X1 by ;
hence P in the topology of X1 by ; :: thesis: verum
end;
hence X1 is SubSpace of X2 by ; :: thesis: verum