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

let V be a_neighborhood of 0. X; :: according to RLTOPSP1:def 12 :: thesis:
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;

suppose A5: r <= s ; :: thesis:

take s ; :: thesis:
thus s > 0 by A1; :: thesis:
let t be Real; :: thesis:
assume A6: t > s ; :: thesis:
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:

end;

suppose A8: r > s ; :: thesis:

take r ; :: thesis:
thus r > 0 by A3; :: thesis:
let t be Real; :: thesis:
assume A9: t > r ; :: thesis:
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:

end;

end;

end;