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) <= () + ()

let P, Q be Subset of T; :: thesis: ( P is bounded & Q is bounded & P meets Q implies diameter (P \/ 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) <= () + ()
set g = the Element of P /\ Q;
A4: the Element of P /\ Q in Q by ;
set s = () + ();
set b = diameter Q;
A5: diameter Q <= () + () by ;
set a = diameter P;
A6: the Element of P /\ Q in P by ;
reconsider g = the Element of P /\ Q as Element of T by ;
A7: diameter P <= () + () by ;
A8: for x, y being Point of T st x in P \/ Q & y in P \/ Q holds
dist (x,y) <= () + ()
proof
let x, y be Point of T; :: thesis: ( x in P \/ Q & y in P \/ Q implies dist (x,y) <= () + () )
assume that
A9: x in P \/ Q and
A10: y in P \/ Q ; :: thesis: dist (x,y) <= () + ()
A11: dist (x,y) <= (dist (x,g)) + (dist (g,y)) by METRIC_1:4;
now :: thesis: dist (x,y) <= () + ()
per cases ( x in P or x in Q ) by ;
suppose A12: x in P ; :: thesis: dist (x,y) <= () + ()
now :: thesis: dist (x,y) <= () + ()
per cases ( y in P or y in Q ) by ;
suppose y in P ; :: thesis: dist (x,y) <= () + ()
then dist (x,y) <= diameter P by ;
hence dist (x,y) <= () + () by ; :: thesis: verum
end;
suppose A13: y in Q ; :: thesis: dist (x,y) <= () + ()
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)) <= () + () by ;
hence dist (x,y) <= () + () by ; :: thesis: verum
end;
end;
end;
hence dist (x,y) <= () + () ; :: thesis: verum
end;
suppose A15: x in Q ; :: thesis: dist (x,y) <= () + ()
now :: thesis: dist (x,y) <= () + ()
per cases ( y in P or y in Q ) by ;
suppose A16: y in P ; :: thesis: dist (x,y) <= () + ()
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)) <= () + () by ;
hence dist (x,y) <= () + () by ; :: thesis: verum
end;
suppose y in Q ; :: thesis: dist (x,y) <= () + ()
then dist (x,y) <= diameter Q by ;
hence dist (x,y) <= () + () by ; :: thesis: verum
end;
end;
end;
hence dist (x,y) <= () + () ; :: thesis: verum
end;
end;
end;
hence dist (x,y) <= () + () ; :: thesis: verum
end;
( P <> {} & P \/ Q is bounded ) by A1, A2, A3, Th13;
hence diameter (P \/ Q) <= () + () by ; :: thesis: verum