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)

proof

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;

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

per cases ( x in P or x in Q ) by A9, XBOOLE_0:def 3;

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

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

per cases ( y in P or y in Q ) by A10, XBOOLE_0:def 3;

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;

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;

end;

end;

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

end;

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

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

per cases ( y in P or y in Q ) by A10, XBOOLE_0:def 3;

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;

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

then dist (x,y) <= diameter Q by A2, A15, Def8;
hence dist (x,y) <= (diameter P) + (diameter Q) by A5, XXREAL_0:2; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

( P <> {} & P \/ Q is bounded ) by A1, A2, A3, Th13;
hence diameter (P \/ Q) <= (diameter P) + (diameter Q) by A8, Def8; :: thesis: verum