let n be 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 Th5;
C = REAL n by EUCLID:22;
hence contradiction by A1, Th20; :: thesis: verum