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 that
A1: P is bounded and
A2: 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 A2; :: thesis: verum
end;
suppose A3: P <> {} ; :: thesis: P \/ Q is bounded
now :: thesis: P \/ Q is bounded
per cases ( Q = {} or Q <> {} ) ;
suppose Q <> {} ; :: thesis: P \/ Q is bounded
then consider s being Real, d being Element of T such that
A4: 0 < s and
d in Q and
A5: for z being Point of T st z in Q holds
dist (d,z) <= s by ;
consider r being Real, t1 being Element of T such that
A6: 0 < r and
A7: t1 in P and
A8: for z being Point of T st z in P holds
dist (t1,z) <= r by A1, A3, Th10;
set t = (r + s) + (dist (t1,d));
A9: 0 <= dist (t1,d) by METRIC_1:5;
then A10: r < r + ((dist (t1,d)) + s) by ;
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
reconsider t = (r + s) + (dist (t1,d)) as Real ;
take t ; :: thesis: 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 ) )

take t1 ; :: thesis: ( 0 < t & t1 in P \/ Q & ( for z being Point of T st z in P \/ Q holds
dist (t1,z) <= t ) )

thus 0 < t by A6, A4, A9; :: thesis: ( t1 in P \/ Q & ( for z being Point of T st z in P \/ Q holds
dist (t1,z) <= t ) )

thus t1 in P \/ Q by ; :: thesis: for z being Point of T st z in P \/ Q holds
dist (t1,z) <= t

let z be Point of T; :: thesis: ( z in P \/ Q implies dist (t1,z) <= t )
assume z in P \/ Q ; :: thesis: dist (t1,z) <= t
then A11: ( z in P or z in Q ) by XBOOLE_0:def 3;
now :: thesis: dist (t1,z) <= t
per cases ( dist (t1,z) <= r or dist (d,z) <= s ) by A8, A5, A11;
suppose dist (t1,z) <= r ; :: thesis: dist (t1,z) <= t
hence dist (t1,z) <= t by ; :: thesis: verum
end;
suppose dist (d,z) <= s ; :: thesis: dist (t1,z) <= t
then ( dist (t1,z) <= (dist (t1,d)) + (dist (d,z)) & (dist (t1,d)) + (dist (d,z)) <= (dist (t1,d)) + s ) by ;
then A12: dist (t1,z) <= (dist (t1,d)) + s by XXREAL_0:2;
(dist (t1,d)) + s <= r + ((dist (t1,d)) + s) by ;
hence dist (t1,z) <= t by ; :: thesis: verum
end;
end;
end;
hence dist (t1,z) <= t ; :: thesis: verum
end;
hence P \/ Q is bounded by Th10; :: thesis: verum
end;
end;
end;
hence P \/ Q is bounded ; :: thesis: verum
end;
end;