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 Th35, Th36;
hence HausDist P,R <= (HausDist P,Q) + (HausDist Q,R) by XXREAL_0:28; :: thesis: verum