let n be Nat; :: thesis: for D being Subset of (TOP-REAL n)
for A, C being non empty Subset of (TOP-REAL n) st C c= D holds
dist_min (A,D) <= dist_min (A,C)
let D be Subset of (TOP-REAL n); :: thesis: for A, C being non empty Subset of (TOP-REAL n) st C c= D holds
dist_min (A,D) <= dist_min (A,C)
let A, C be non empty Subset of (TOP-REAL n); :: thesis: ( C c= D implies dist_min (A,D) <= dist_min (A,C) )
assume A1: C c= D ; :: thesis: dist_min (A,D) <= dist_min (A,C)
consider A9, D9 being Subset of (TopSpaceMetr (Euclid n)) such that
A2: A = A9 and
A3: ( D = D9 & dist_min (A,D) = min_dist_min (A9,D9) ) by Def1;
reconsider f = dist_min A9 as Function of the carrier of (TopSpaceMetr (Euclid n)),REAL by TOPMETR:17;
reconsider Y = f .: D9 as Subset of REAL ;
A4: Y is bounded_below
proof
take 0 ; :: according to XXREAL_2:def 9 :: thesis: 0 is LowerBound of Y
let r be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not r in Y or 0 <= r )
assume r in Y ; :: thesis: 0 <= r
then ex c being Element of (TopSpaceMetr (Euclid n)) st
( c in D9 & r = f . c ) by FUNCT_2:65;
hence 0 <= r by A2, Th9; :: thesis: verum
end;
A5: lower_bound Y = lower_bound ([#] ((dist_min A9) .: D9)) by WEIERSTR:def 1
.= lower_bound ((dist_min A9) .: D9) by WEIERSTR:def 3
.= min_dist_min (A9,D9) by WEIERSTR:def 7 ;
consider A99, C9 being Subset of (TopSpaceMetr (Euclid n)) such that
A6: A = A99 and
A7: C = C9 and
A8: dist_min (A,C) = min_dist_min (A99,C9) by Def1;
dom f = the carrier of (TopSpaceMetr (Euclid n)) by FUNCT_2:def 1;
then reconsider X = f .: C9 as non empty Subset of REAL by A7;
lower_bound X = lower_bound ([#] ((dist_min A9) .: C9)) by WEIERSTR:def 1
.= lower_bound ((dist_min A9) .: C9) by WEIERSTR:def 3
.= min_dist_min (A9,C9) by WEIERSTR:def 7 ;
hence dist_min (A,D) <= dist_min (A,C) by A1, A2, A3, A6, A7, A8, A5, A4, RELAT_1:123, SEQ_4:47; :: thesis: verum