:: deftheorem Def12 defines bounded RLTOPSP1:def 12 :
for X being LinearTopSpace
for E being Subset of X holds
( E is bounded iff for V being a_neighborhood of 0. X ex s being Real st
( s > 0 & ( for t being Real st t > s holds
E c= t * V ) ) );