let M be non empty MetrSpace; :: thesis: for P, Q being non empty Subset of (TopSpaceMetr M) st P is compact & Q is compact holds
HausDist (P,Q) >= 0
let P, Q be non empty Subset of (TopSpaceMetr M); :: thesis: ( P is compact & Q is compact implies HausDist (P,Q) >= 0 )
assume A1: ( P is compact & Q is compact ) ; :: thesis: HausDist (P,Q) >= 0

per cases ( HausDist (P,Q) = max_dist_min (P,Q) or HausDist (P,Q) = max_dist_min (Q,P) ) by XXREAL_0:16;

suppose HausDist (P,Q) = max_dist_min (P,Q) ; :: thesis: HausDist (P,Q) >= 0

hence HausDist (P,Q) >= 0 by A1, Th28; :: thesis: verum

end;

suppose HausDist (P,Q) = max_dist_min (Q,P) ; :: thesis: HausDist (P,Q) >= 0

hence HausDist (P,Q) >= 0 by A1, Th28; :: thesis: verum

end;

end;