for X being TopSpace
for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is open SubSpace of X iff A is open )