let S be Subset of X; :: thesis: ( S is empty implies S is bounded )
assume S is empty ; :: thesis: S is bounded
then A1: 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 1 ; :: thesis: ( 1 > 0 & ( for t being Real st t > 1 holds
S c= t * V ) )
thus ( 1 > 0 & ( for t being Real st t > 1 holds
S c= t * V ) ) by A1; :: thesis: verum