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 that
A1: P is compact and
A2: Q is compact and
A3: R is compact ; :: thesis: HausDist P,R <= (HausDist P,Q) + (HausDist Q,R)
A4: max_dist_min P,R <= (HausDist P,Q) + (HausDist Q,R) by A1, A2, A3, Th35;
max_dist_min R,P <= (HausDist P,Q) + (HausDist Q,R) by A1, A2, A3, Th36;
hence HausDist P,R <= (HausDist P,Q) + (HausDist Q,R) by A4, XXREAL_0:28; :: thesis: verum