let S be Subset of X; :: thesis: ( S is empty implies S is bounded )
assume S is empty ; :: thesis: S is bounded
then X: S = {} X ;
let V be a_neighborhood of 0. X; :: according to RLTOPSP1:def 12 :: thesis: ex s being Real st
( s > 0 & ( for t being Real st t > s holds
S c= t * V ) )
take s = 1; :: thesis: ( s > 0 & ( for t being Real st t > s holds
S c= t * V ) )
thus ( s > 0 & ( for t being Real st t > s holds
S c= t * V ) ) by XBOOLE_1:2, X; :: thesis: verum