let n be Nat; :: thesis: for S being Subset of (TOP-REAL n) holds
( not S is bounded iff for r being Real st r > 0 holds
ex x, y being Point of (Euclid n) st
( x in S & y in S & dist (x,y) > r ) )
let S be Subset of (TOP-REAL n); :: thesis: ( not S is bounded iff for r being Real st r > 0 holds
ex x, y being Point of (Euclid n) st
( x in S & y in S & dist (x,y) > r ) )
reconsider S9 = S as Subset of (Euclid n) by TOPREAL3:8;

hereby :: thesis: ( ( for r being Real st r > 0 holds
ex x, y being Point of (Euclid n) st
( x in S & y in S & dist (x,y) > r ) ) implies not S is bounded )

assume not S is bounded ; :: thesis: for r being Real st r > 0 holds
ex x, y being Point of (Euclid n) st
( x in S & y in S & dist (x,y) > r )
then not S9 is bounded by JORDAN2C:11;
hence for r being Real st r > 0 holds
ex x, y being Point of (Euclid n) st
( x in S & y in S & dist (x,y) > r ) by TBSP_1:def 7; :: thesis: verum

end;

assume A1: for r being Real st r > 0 holds
ex x, y being Point of (Euclid n) st
( x in S & y in S & dist (x,y) > r ) ; :: thesis: not S is bounded
not S is bounded

proof

assume S is bounded ; :: thesis: contradiction
then S is bounded Subset of (Euclid n) by JORDAN2C:11;
hence contradiction by A1, TBSP_1:def 7; :: thesis: verum

end;

hence not S is bounded ; :: thesis: verum