let T be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: for P, Q being Subset of T st P is bounded & Q is bounded holds
P \/ Q is bounded
let P, Q be Subset of T; :: thesis: ( P is bounded & Q is bounded implies P \/ Q is bounded )
assume A1: ( P is bounded & Q is bounded ) ; :: thesis: P \/ Q is bounded

per cases ( P = {} or P <> {} ) ;

suppose P = {} ; :: thesis: P \/ Q is bounded

hence P \/ Q is bounded by A1; :: thesis: verum

end;

suppose A2: P <> {} ; :: thesis: P \/ Q is bounded

now

per cases ( Q = {} or Q <> {} ) ;

suppose Q = {} ; :: thesis: P \/ Q is bounded

hence P \/ Q is bounded by A1; :: thesis: verum

end;

suppose A3: Q <> {} ; :: thesis: P \/ Q is bounded

consider r being Real, t1 being Element of T such that
A4: ( 0 < r & t1 in P & ( for z being Point of T st z in P holds
dist t1,z <= r ) ) by A1, A2, Th15;
consider s being Real, d being Element of T such that
A5: ( 0 < s & d in Q & ( for z being Point of T st z in Q holds
dist d,z <= s ) ) by A1, A3, Th15;
set t = (r + s) + (dist t1,d);
A6: dist t1,d < (dist t1,d) + s by A5, XREAL_1:31;
0 <= dist t1,d by METRIC_1:5;
then A7: r < r + ((dist t1,d) + s) by A6, XREAL_1:31;
ex t being Real ex t1 being Element of T st
( 0 < t & t1 in P \/ Q & ( for z being Point of T st z in P \/ Q holds
dist t1,z <= t ) )

proof

take (r + s) + (dist t1,d) ; :: thesis: ex t1 being Element of T st
( 0 < (r + s) + (dist t1,d) & t1 in P \/ Q & ( for z being Point of T st z in P \/ Q holds
dist t1,z <= (r + s) + (dist t1,d) ) )
take t1 ; :: thesis: ( 0 < (r + s) + (dist t1,d) & t1 in P \/ Q & ( for z being Point of T st z in P \/ Q holds
dist t1,z <= (r + s) + (dist t1,d) ) )
thus 0 < (r + s) + (dist t1,d) by A4, A7; :: thesis: ( t1 in P \/ Q & ( for z being Point of T st z in P \/ Q holds
dist t1,z <= (r + s) + (dist t1,d) ) )
thus t1 in P \/ Q by A4, XBOOLE_0:def 3; :: thesis: for z being Point of T st z in P \/ Q holds
dist t1,z <= (r + s) + (dist t1,d)
let z be Point of T; :: thesis: ( z in P \/ Q implies dist t1,z <= (r + s) + (dist t1,d) )
assume z in P \/ Q ; :: thesis: dist t1,z <= (r + s) + (dist t1,d)
then A8: ( z in P or z in Q ) by XBOOLE_0:def 3;

now

per cases ( dist t1,z <= r or dist d,z <= s ) by A4, A5, A8;

suppose dist t1,z <= r ; :: thesis: dist t1,z <= (r + s) + (dist t1,d)

hence dist t1,z <= (r + s) + (dist t1,d) by A7, XXREAL_0:2; :: thesis: verum

end;

suppose A9: dist d,z <= s ; :: thesis: dist t1,z <= (r + s) + (dist t1,d)

A10: dist t1,z <= (dist t1,d) + (dist d,z) by METRIC_1:4;
(dist t1,d) + (dist d,z) <= (dist t1,d) + s by A9, XREAL_1:9;
then A11: dist t1,z <= (dist t1,d) + s by A10, XXREAL_0:2;
(dist t1,d) + s <= r + ((dist t1,d) + s) by A4, XREAL_1:31;
hence dist t1,z <= (r + s) + (dist t1,d) by A11, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence dist t1,z <= (r + s) + (dist t1,d) ; :: thesis: verum

end;

hence P \/ Q is bounded by Th15; :: thesis: verum

end;

end;

end;

hence P \/ Q is bounded ; :: thesis: verum

end;

end;