let T be TopSpace; :: thesis: for A, B being SubSpace of T st the carrier of A c= the carrier of B holds
A is SubSpace of B
let A, B be SubSpace of T; :: thesis: ( the carrier of A c= the carrier of B implies A is SubSpace of B )
assume A1: the carrier of A c= the carrier of B ; :: thesis: A is SubSpace of B
then A2: the carrier of A c= [#] B ;
for P being Subset of A holds
( P in the topology of A iff ex Q being Subset of B st
( Q in the topology of B & P = Q /\ ([#] A) ) )

proof

let P be Subset of A; :: thesis: ( P in the topology of A iff ex Q being Subset of B st
( Q in the topology of B & P = Q /\ ([#] A) ) )
thus ( P in the topology of A implies ex Q being Subset of B st
( Q in the topology of B & P = Q /\ ([#] A) ) ) :: thesis: ( ex Q being Subset of B st
( Q in the topology of B & P = Q /\ ([#] A) ) implies P in the topology of A )

proof

assume P in the topology of A ; :: thesis: ex Q being Subset of B st
( Q in the topology of B & P = Q /\ ([#] A) )
then consider Q' being Subset of T such that
A3: ( Q' in the topology of T & P = Q' /\ ([#] A) ) by PRE_TOPC:def 9;
reconsider Q = Q' /\ ([#] B) as Subset of B ;
A4: Q in the topology of B by A3, PRE_TOPC:def 9;
P = Q' /\ (([#] B) /\ ([#] A)) by A1, A3, XBOOLE_1:28
.= Q /\ ([#] A) by XBOOLE_1:16 ;
hence ex Q being Subset of B st
( Q in the topology of B & P = Q /\ ([#] A) ) by A4; :: thesis: verum

end;

given Q being Subset of B such that A5: ( Q in the topology of B & P = Q /\ ([#] A) ) ; :: thesis: P in the topology of A
consider P' being Subset of T such that
A6: ( P' in the topology of T & Q = P' /\ ([#] B) ) by A5, PRE_TOPC:def 9;
P = P' /\ (([#] B) /\ ([#] A)) by A5, A6, XBOOLE_1:16
.= P' /\ ([#] A) by A1, XBOOLE_1:28 ;
hence P in the topology of A by A6, PRE_TOPC:def 9; :: thesis: verum

end;

hence A is SubSpace of B by A2, PRE_TOPC:def 9; :: thesis: verum