let n be Element of NAT ; :: thesis: for P, Q, R being non empty Subset of (TOP-REAL n) 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 (TOP-REAL n); :: thesis: ( P is compact & Q is compact & R is compact implies HausDist P,R <= (HausDist P,Q) + (HausDist Q,R) )
assume A1: ( P is compact & Q is compact & R is compact ) ; :: thesis: HausDist P,R <= (HausDist P,Q) + (HausDist Q,R)
X: TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider P1 = P, Q1 = Q, R1 = R as non empty Subset of (TopSpaceMetr (Euclid n)) ;
Y: ( P1 is compact & Q1 is compact & R1 is compact ) by A1, COMPTS_1:33, X;
( HausDist P1,R1 = HausDist P,R & HausDist P1,Q1 = HausDist P,Q & HausDist Q1,R1 = HausDist Q,R ) by Def3;
hence HausDist P,R <= (HausDist P,Q) + (HausDist Q,R) by A1, Th40, Y; :: thesis: verum