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 Def2;
C = REAL n by EUCLID:25;
hence contradiction by A1, Th39; :: thesis: verum