for X being non empty TopSpace
for X0 being non empty SubSpace of X
for X1, X2 being SubSpace of X
for Y1, Y2 being SubSpace of X0 st the carrier of X1 = the carrier of Y1 & the carrier of X2 = the carrier of Y2 holds
( X1,X2 are_separated iff Y1,Y2 are_separated )