for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X
for x being Point of (X1 union X2) holds
( ex x1 being Point of X1 st x1 = x or ex x2 being Point of X2 st x2 = x )