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

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

end;

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 A2, Th10;
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 A4, XREAL_1:29;
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 A7, XBOOLE_0:def 3; :: 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 A10, XXREAL_0:2; :: 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 METRIC_1:4, XREAL_1:7;
then A12: dist (t1,z) <= (dist (t1,d)) + s by XXREAL_0:2;
(dist (t1,d)) + s <= r + ((dist (t1,d)) + s) by A6, XREAL_1:29;
hence dist (t1,z) <= t by A12, XXREAL_0:2; :: 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;