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

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 <> {} )
;

end;

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

end;

now :: thesis: P \/ Q is bounded end;

hence
P \/ Q is bounded
; :: thesis: verumper cases
( Q = {} or Q <> {} )
;

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 ) )

end;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

hence
P \/ Q is bounded
by Th10; :: thesis: verum
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;

end;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) <= tend;

hence
dist (t1,z) <= t
; :: thesis: verumper cases
( dist (t1,z) <= r or dist (d,z) <= s )
by A8, A5, A11;

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;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