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 that
A1: ( P is compact & Q is compact ) and
A2: R is compact ; :: thesis: HausDist (P,R) <= (HausDist (P,Q)) + (HausDist (Q,R))
A3: 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)) ;
A4: R1 is compact by A2, A3, COMPTS_1:33;
A5: HausDist (Q1,R1) = HausDist (Q,R) by Def3;
A6: ( HausDist (P1,R1) = HausDist (P,R) & HausDist (P1,Q1) = HausDist (P,Q) ) by Def3;
( P1 is compact & Q1 is compact ) by A1, A3, COMPTS_1:33;
hence HausDist (P,R) <= (HausDist (P,Q)) + (HausDist (Q,R)) by A4, A6, A5, Th40; :: thesis: verum