let T1, T2, S1, S2 be TopStruct ; :: thesis: ( TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) & TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of S2, the topology of S2 #) & S1 is SubSpace of T1 implies S2 is SubSpace of T2 )
assume A1: ( TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) & TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of S2, the topology of S2 #) ) ; :: thesis: ( not S1 is SubSpace of T1 or S2 is SubSpace of T2 )
assume that
A2: [#] S1 c= [#] T1 and
A3: for P being Subset of S1 holds
( P in the topology of S1 iff ex Q being Subset of T1 st
( Q in the topology of T1 & P = Q /\ ([#] S1) ) ) ; :: according to PRE_TOPC:def 4 :: thesis: S2 is SubSpace of T2
thus [#] S2 c= [#] T2 by A1, A2; :: according to PRE_TOPC:def 4 :: thesis: for P being Subset of S2 holds
( P in the topology of S2 iff ex Q being Subset of T2 st
( Q in the topology of T2 & P = Q /\ ([#] S2) ) )
thus for P being Subset of S2 holds
( P in the topology of S2 iff ex Q being Subset of T2 st
( Q in the topology of T2 & P = Q /\ ([#] S2) ) ) by A1, A3; :: thesis: verum