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, Th30; :: thesis: verum

end;

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

hence HausDist P,Q >= 0 by A1, Th30; :: thesis: verum

end;

end;