theorem :: TOPREAL6:66

for n being Nat
for X, Y being Subset of (TOP-REAL n) st n >= 1 & the carrier of (TOP-REAL n) = X \/ Y & X is bounded holds
not Y is bounded