let X be LinearTopSpace; :: thesis: for E being bounded Subset of X holds Cl E is bounded
let E be bounded Subset of X; :: thesis: Cl E is bounded
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
Cl E c= t * V ) )
consider W being a_neighborhood of 0. X such that
A1: Cl W c= V by Th59;
consider s being Real such that
A2: s > 0 and
A3: for t being Real st t > s holds
E c= t * W by Def12;
take s ; :: thesis: ( s > 0 & ( for t being Real st t > s holds
Cl E c= t * V ) )
thus s > 0 by A2; :: thesis: for t being Real st t > s holds
Cl E c= t * V
let t be Real; :: thesis: ( t > s implies Cl E c= t * V )
assume t > s ; :: thesis: Cl E c= t * V
then A4: ( Cl E c= Cl (t * W) & Cl (t * W) = t * (Cl W) ) by A2, A3, Th52, PRE_TOPC:19;
t * (Cl W) c= t * V by A1, CONVEX1:39;
hence Cl E c= t * V by A4; :: thesis: verum