let n be Nat; :: thesis: 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
set M = TOP-REAL n;
let X, Y be Subset of (TOP-REAL n); :: thesis: ( n >= 1 & the carrier of (TOP-REAL n) = X \/ Y & X is bounded implies not Y is bounded )
assume that
A1: n >= 1 and
A2: the carrier of (TOP-REAL n) = X \/ Y ; :: thesis: ( not X is bounded or not Y is bounded )
reconsider E = [#] (TOP-REAL n) as Subset of (Euclid n) by TOPREAL3:8;
not [#] (TOP-REAL n) is bounded by A1, JORDAN2C:35;
then A3: not E is bounded by JORDAN2C:11;
reconsider D = Y as Subset of (Euclid n) by TOPREAL3:8;
assume X is bounded ; :: thesis: not Y is bounded
then reconsider C = X as bounded Subset of (Euclid n) by JORDAN2C:11;
A4: the carrier of (Euclid n) = C \/ D by A2, TOPREAL3:8;
E = [#] (Euclid n) by TOPREAL3:8;
then not Euclid n is bounded by A3;
then not D is bounded by A4, Th63;
hence not Y is bounded by JORDAN2C:11; :: thesis: verum