let X be LinearTopSpace; :: thesis: for P being bounded Subset of X
for Q being Subset of X st Q c= P holds
Q is bounded
let P be bounded Subset of X; :: thesis: for Q being Subset of X st Q c= P holds
Q is bounded
let Q be Subset of X; :: thesis: ( Q c= P implies Q is bounded )
assume A1: Q c= P ; :: thesis: Q 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
Q c= t * V ) )
consider s being Real such that
A2: s > 0 and
A3: for t being Real st t > s holds
P c= t * V by Def12;
take s ; :: thesis: ( s > 0 & ( for t being Real st t > s holds
Q c= t * V ) )
thus s > 0 by A2; :: thesis: for t being Real st t > s holds
Q c= t * V
let t be Real; :: thesis: ( t > s implies Q c= t * V )
assume t > s ; :: thesis: Q c= t * V
then P c= t * V by A3;
hence Q c= t * V by A1; :: thesis: verum