let n be Element of NAT ; :: thesis: ( n >= 1 implies not [#] (TOP-REAL n) is bounded )
assume A1: n >= 1 ; :: thesis: not [#] (TOP-REAL n) is bounded
assume [#] (TOP-REAL n) is bounded ; :: thesis: contradiction
then reconsider C = [#] (TOP-REAL n) as bounded Subset of (Euclid n) by Th11;
C = REAL n by EUCLID:22;
hence contradiction by A1, Th33; :: thesis: verum