let n be Element of 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:def 1;
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:def 1;
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, Th73;
hence not Y is Bounded by JORDAN2C:def 1; :: thesis: verum