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)
consider g being Element of P /\ Q;
A4: g 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, Th29, XREAL_1:33;
set a = diameter P;
A6: g in P by A3, XBOOLE_0:def 4;
reconsider g = g as Element of T by A3, TARSKI:def 3;
A7: diameter P <= (diameter P) + (diameter Q) by A2, Th29, XREAL_1:33;
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

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

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, Def10;
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, Def10;
dist g,y <= diameter Q by A2, A4, A13, Def10;
then (dist x,g) + (dist g,y) <= (diameter P) + (diameter Q) by A14, XREAL_1:9;
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

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, Def10;
dist g,y <= diameter P by A1, A6, A16, Def10;
then (dist x,g) + (dist g,y) <= (diameter Q) + (diameter P) by A17, XREAL_1:9;
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, Def10;
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, Th20;
hence diameter (P \/ Q) <= (diameter P) + (diameter Q) by A8, Def10; :: thesis: verum