let X be TopStruct ; :: thesis: for X1, X2 being TopSpace st X1 = TopStruct(# the carrier of X2, the topology of X2 #) holds

( X1 is SubSpace of X iff X2 is SubSpace of X )

let X1, X2 be TopSpace; :: thesis: ( X1 = TopStruct(# the carrier of X2, the topology of X2 #) implies ( X1 is SubSpace of X iff X2 is SubSpace of X ) )

assume A1: X1 = TopStruct(# the carrier of X2, the topology of X2 #) ; :: thesis: ( X1 is SubSpace of X iff X2 is SubSpace of X )

thus ( X1 is SubSpace of X implies X2 is SubSpace of X ) :: thesis: ( X2 is SubSpace of X implies X1 is SubSpace of X )

( X1 is SubSpace of X iff X2 is SubSpace of X )

let X1, X2 be TopSpace; :: thesis: ( X1 = TopStruct(# the carrier of X2, the topology of X2 #) implies ( X1 is SubSpace of X iff X2 is SubSpace of X ) )

assume A1: X1 = TopStruct(# the carrier of X2, the topology of X2 #) ; :: thesis: ( X1 is SubSpace of X iff X2 is SubSpace of X )

thus ( X1 is SubSpace of X implies X2 is SubSpace of X ) :: thesis: ( X2 is SubSpace of X implies X1 is SubSpace of X )

proof

thus
( X2 is SubSpace of X implies X1 is SubSpace of X )
by A1, Th6; :: thesis: verum
A2:
[#] X1 = the carrier of X1
;

assume A3: X1 is SubSpace of X ; :: thesis: X2 is SubSpace of X

hence [#] X2 c= [#] X by A1, A2, PRE_TOPC:def 4; :: according to PRE_TOPC:def 4 :: thesis: for b_{1} being Element of bool the carrier of X2 holds

( ( not b_{1} in the topology of X2 or ex b_{2} being Element of bool the carrier of X st

( b_{2} in the topology of X & b_{1} = b_{2} /\ ([#] X2) ) ) & ( for b_{2} being Element of bool the carrier of X holds

( not b_{2} in the topology of X or not b_{1} = b_{2} /\ ([#] X2) ) or b_{1} in the topology of X2 ) )

let P be Subset of X2; :: thesis: ( ( not P in the topology of X2 or ex b_{1} being Element of bool the carrier of X st

( b_{1} in the topology of X & P = b_{1} /\ ([#] X2) ) ) & ( for b_{1} being Element of bool the carrier of X holds

( not b_{1} in the topology of X or not P = b_{1} /\ ([#] X2) ) or P in the topology of X2 ) )

thus ( P in the topology of X2 implies ex Q being Subset of X st

( Q in the topology of X & P = Q /\ ([#] X2) ) ) by A1, A3, A2, PRE_TOPC:def 4; :: thesis: ( for b_{1} being Element of bool the carrier of X holds

( not b_{1} in the topology of X or not P = b_{1} /\ ([#] X2) ) or P in the topology of X2 )

given Q being Subset of X such that A4: ( Q in the topology of X & P = Q /\ ([#] X2) ) ; :: thesis: P in the topology of X2

thus P in the topology of X2 by A1, A3, A2, A4, PRE_TOPC:def 4; :: thesis: verum

end;assume A3: X1 is SubSpace of X ; :: thesis: X2 is SubSpace of X

hence [#] X2 c= [#] X by A1, A2, PRE_TOPC:def 4; :: according to PRE_TOPC:def 4 :: thesis: for b

( ( not b

( b

( not b

let P be Subset of X2; :: thesis: ( ( not P in the topology of X2 or ex b

( b

( not b

thus ( P in the topology of X2 implies ex Q being Subset of X st

( Q in the topology of X & P = Q /\ ([#] X2) ) ) by A1, A3, A2, PRE_TOPC:def 4; :: thesis: ( for b

( not b

given Q being Subset of X such that A4: ( Q in the topology of X & P = Q /\ ([#] X2) ) ; :: thesis: P in the topology of X2

thus P in the topology of X2 by A1, A3, A2, A4, PRE_TOPC:def 4; :: thesis: verum