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
A2: 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 Q9 being Subset of T such that
A3: Q9 in the topology of T and
A4: P = Q9 /\ ([#] A) by PRE_TOPC:def 4;
reconsider Q = Q9 /\ ([#] B) as Subset of B ;
A5: Q in the topology of B by A3, PRE_TOPC:def 4;
P = Q9 /\ (([#] B) /\ ([#] A)) by A1, A4, 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 A5; :: thesis: verum
end;
given Q being Subset of B such that A6: Q in the topology of B and
A7: P = Q /\ ([#] A) ; :: thesis: P in the topology of A
consider P9 being Subset of T such that
A8: P9 in the topology of T and
A9: Q = P9 /\ ([#] B) by A6, PRE_TOPC:def 4;
P = P9 /\ (([#] B) /\ ([#] A)) by A7, A9, XBOOLE_1:16
.= P9 /\ ([#] A) by A1, XBOOLE_1:28 ;
hence P in the topology of A by A8, PRE_TOPC:def 4; :: thesis: verum
end;
the carrier of A c= [#] B by A1;
hence A is SubSpace of B by A2, PRE_TOPC:def 4; :: thesis: verum