let T be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: for P, Q being Subset of T st P is bounded & Q is bounded & P meets Q holds

diameter (P \/ Q) <= (diameter P) + (diameter Q)

let P, Q be Subset of T; :: thesis: ( P is bounded & Q is bounded & P meets Q implies diameter (P \/ Q) <= (diameter P) + (diameter Q) )

assume that

A1: P is bounded and

A2: Q is bounded and

A3: P /\ Q <> {} ; :: according to XBOOLE_0:def 7 :: thesis: diameter (P \/ Q) <= (diameter P) + (diameter Q)

set g = the Element of P /\ Q;

A4: the Element of P /\ Q in Q by A3, XBOOLE_0:def 4;

set s = (diameter P) + (diameter Q);

set b = diameter Q;

A5: diameter Q <= (diameter P) + (diameter Q) by A1, Th21, XREAL_1:31;

set a = diameter P;

A6: the Element of P /\ Q in P by A3, XBOOLE_0:def 4;

reconsider g = the Element of P /\ Q as Element of T by A3, TARSKI:def 3;

A7: diameter P <= (diameter P) + (diameter Q) by A2, Th21, XREAL_1:31;

A8: for x, y being Point of T st x in P \/ Q & y in P \/ Q holds

dist (x,y) <= (diameter P) + (diameter Q)

hence diameter (P \/ Q) <= (diameter P) + (diameter Q) by A8, Def8; :: thesis: verum

diameter (P \/ Q) <= (diameter P) + (diameter Q)

let P, Q be Subset of T; :: thesis: ( P is bounded & Q is bounded & P meets Q implies diameter (P \/ Q) <= (diameter P) + (diameter Q) )

assume that

A1: P is bounded and

A2: Q is bounded and

A3: P /\ Q <> {} ; :: according to XBOOLE_0:def 7 :: thesis: diameter (P \/ Q) <= (diameter P) + (diameter Q)

set g = the Element of P /\ Q;

A4: the Element of P /\ Q in Q by A3, XBOOLE_0:def 4;

set s = (diameter P) + (diameter Q);

set b = diameter Q;

A5: diameter Q <= (diameter P) + (diameter Q) by A1, Th21, XREAL_1:31;

set a = diameter P;

A6: the Element of P /\ Q in P by A3, XBOOLE_0:def 4;

reconsider g = the Element of P /\ Q as Element of T by A3, TARSKI:def 3;

A7: diameter P <= (diameter P) + (diameter Q) by A2, Th21, XREAL_1:31;

A8: for x, y being Point of T st x in P \/ Q & y in P \/ Q holds

dist (x,y) <= (diameter P) + (diameter Q)

proof

( P <> {} & P \/ Q is bounded )
by A1, A2, A3, Th13;
let x, y be Point of T; :: thesis: ( x in P \/ Q & y in P \/ Q implies dist (x,y) <= (diameter P) + (diameter Q) )

assume that

A9: x in P \/ Q and

A10: y in P \/ Q ; :: thesis: dist (x,y) <= (diameter P) + (diameter Q)

A11: dist (x,y) <= (dist (x,g)) + (dist (g,y)) by METRIC_1:4;

end;assume that

A9: x in P \/ Q and

A10: y in P \/ Q ; :: thesis: dist (x,y) <= (diameter P) + (diameter Q)

A11: dist (x,y) <= (dist (x,g)) + (dist (g,y)) by METRIC_1:4;

now :: thesis: dist (x,y) <= (diameter P) + (diameter Q)end;

hence
dist (x,y) <= (diameter P) + (diameter Q)
; :: thesis: verumper cases
( x in P or x in Q )
by A9, XBOOLE_0:def 3;

end;

suppose A12:
x in P
; :: thesis: dist (x,y) <= (diameter P) + (diameter Q)

end;

now :: thesis: dist (x,y) <= (diameter P) + (diameter Q)end;

hence
dist (x,y) <= (diameter P) + (diameter Q)
; :: thesis: verumper cases
( y in P or y in Q )
by A10, XBOOLE_0:def 3;

end;

suppose
y in P
; :: thesis: dist (x,y) <= (diameter P) + (diameter Q)

then
dist (x,y) <= diameter P
by A1, A12, Def8;

hence dist (x,y) <= (diameter P) + (diameter Q) by A7, XXREAL_0:2; :: thesis: verum

end;hence dist (x,y) <= (diameter P) + (diameter Q) by A7, XXREAL_0:2; :: thesis: verum

suppose A13:
y in Q
; :: thesis: dist (x,y) <= (diameter P) + (diameter Q)

A14:
dist (x,g) <= diameter P
by A1, A6, A12, Def8;

dist (g,y) <= diameter Q by A2, A4, A13, Def8;

then (dist (x,g)) + (dist (g,y)) <= (diameter P) + (diameter Q) by A14, XREAL_1:7;

hence dist (x,y) <= (diameter P) + (diameter Q) by A11, XXREAL_0:2; :: thesis: verum

end;dist (g,y) <= diameter Q by A2, A4, A13, Def8;

then (dist (x,g)) + (dist (g,y)) <= (diameter P) + (diameter Q) by A14, XREAL_1:7;

hence dist (x,y) <= (diameter P) + (diameter Q) by A11, XXREAL_0:2; :: thesis: verum

suppose A15:
x in Q
; :: thesis: dist (x,y) <= (diameter P) + (diameter Q)

end;

now :: thesis: dist (x,y) <= (diameter P) + (diameter Q)end;

hence
dist (x,y) <= (diameter P) + (diameter Q)
; :: thesis: verumper cases
( y in P or y in Q )
by A10, XBOOLE_0:def 3;

end;

suppose A16:
y in P
; :: thesis: dist (x,y) <= (diameter P) + (diameter Q)

A17:
dist (x,g) <= diameter Q
by A2, A4, A15, Def8;

dist (g,y) <= diameter P by A1, A6, A16, Def8;

then (dist (x,g)) + (dist (g,y)) <= (diameter Q) + (diameter P) by A17, XREAL_1:7;

hence dist (x,y) <= (diameter P) + (diameter Q) by A11, XXREAL_0:2; :: thesis: verum

end;dist (g,y) <= diameter P by A1, A6, A16, Def8;

then (dist (x,g)) + (dist (g,y)) <= (diameter Q) + (diameter P) by A17, XREAL_1:7;

hence dist (x,y) <= (diameter P) + (diameter Q) by A11, XXREAL_0:2; :: thesis: verum

hence diameter (P \/ Q) <= (diameter P) + (diameter Q) by A8, Def8; :: thesis: verum