let n be Element of 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:def 1;
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:def 1;
hence contradiction by A1, TBSP_1:def 7; :: thesis: verum

end;

hence not S is Bounded ; :: thesis: verum