for X, X1, X2 being TopSpace st X2 = TopStruct(# the carrier of X1, the topology of X1 #) holds
( X1 is open SubSpace of X iff X2 is open SubSpace of X )