let X be LinearTopSpace; :: thesis: for V1, V2 being bounded Subset of X holds V1 \/ V2 is bounded
let V1, V2 be bounded Subset of X; :: thesis: V1 \/ V2 is bounded
thus V1 \/ V2 is bounded :: thesis: verum

proof

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
V1 \/ V2 c= t * V ) )
consider s being Real such that
A1: s > 0 and
A2: for t being Real st t > s holds
V1 c= t * V by Def12;
consider r being Real such that
A3: r > 0 and
A4: for t being Real st t > r holds
V2 c= t * V by Def12;

per cases ( r <= s or r > s ) ;

suppose A5: r <= s ; :: thesis: ex s being Real st
( s > 0 & ( for t being Real st t > s holds
V1 \/ V2 c= t * V ) )

take s ; :: thesis: ( s > 0 & ( for t being Real st t > s holds
V1 \/ V2 c= t * V ) )
thus s > 0 by A1; :: thesis: for t being Real st t > s holds
V1 \/ V2 c= t * V
let t be Real; :: thesis: ( t > s implies V1 \/ V2 c= t * V )
assume A6: t > s ; :: thesis: V1 \/ V2 c= t * V
t > r by A5, A6, XXREAL_0:2;
then A7: V2 c= t * V by A4;
V1 c= t * V by A2, A6;
hence V1 \/ V2 c= t * V by A7, XBOOLE_1:8; :: thesis: verum

end;

suppose A8: r > s ; :: thesis: ex s being Real st
( s > 0 & ( for t being Real st t > s holds
V1 \/ V2 c= t * V ) )

take r ; :: thesis: ( r > 0 & ( for t being Real st t > r holds
V1 \/ V2 c= t * V ) )
thus r > 0 by A3; :: thesis: for t being Real st t > r holds
V1 \/ V2 c= t * V
let t be Real; :: thesis: ( t > r implies V1 \/ V2 c= t * V )
assume A9: t > r ; :: thesis: V1 \/ V2 c= t * V
t > s by A8, A9, XXREAL_0:2;
then A10: V1 c= t * V by A2;
V2 c= t * V by A4, A9;
hence V1 \/ V2 c= t * V by A10, XBOOLE_1:8; :: thesis: verum

end;

end;

end;