let M be non empty MetrSpace; :: thesis: for P, Q, R being non empty Subset of (TopSpaceMetr M) st P is compact & Q is compact & R is compact holds
HausDist (P,R) <= (HausDist (P,Q)) + (HausDist (Q,R))
let P, Q, R be non empty Subset of (TopSpaceMetr M); :: thesis: ( P is compact & Q is compact & R is compact implies HausDist (P,R) <= (HausDist (P,Q)) + (HausDist (Q,R)) )
assume ( P is compact & Q is compact & R is compact ) ; :: thesis: HausDist (P,R) <= (HausDist (P,Q)) + (HausDist (Q,R))
then ( max_dist_min (P,R) <= (HausDist (P,Q)) + (HausDist (Q,R)) & max_dist_min (R,P) <= (HausDist (P,Q)) + (HausDist (Q,R)) ) by Th33;
hence HausDist (P,R) <= (HausDist (P,Q)) + (HausDist (Q,R)) by XXREAL_0:28; :: thesis: verum