let n be Element of 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 A', D' being Subset of (TopSpaceMetr (Euclid n)) such that
A2: A = A' and
A3: D = D' and
A4: dist_min A,D = min_dist_min A',D' by Def1;
consider A'', C' being Subset of (TopSpaceMetr (Euclid n)) such that
A5: A = A'' and
A6: C = C' and
A7: dist_min A,C = min_dist_min A'',C' by Def1;
reconsider f = dist_min A' as Function of the carrier of (TopSpaceMetr (Euclid n)),REAL by TOPMETR:24;
dom f = the carrier of (TopSpaceMetr (Euclid n)) by FUNCT_2:def 1;
then reconsider X = f .: C' as non empty Subset of REAL by A6;
reconsider Y = f .: D' as Subset of REAL ;
A8: inf Y = lower_bound ([#] ((dist_min A') .: D')) by WEIERSTR:def 3
.= lower_bound ((dist_min A') .: D') by WEIERSTR:def 5
.= min_dist_min A',D' by WEIERSTR:def 9 ;
A9: inf X = lower_bound ([#] ((dist_min A') .: C')) by WEIERSTR:def 3
.= lower_bound ((dist_min A') .: C') by WEIERSTR:def 5
.= min_dist_min A',C' by WEIERSTR:def 9 ;
Y is bounded_below

proof

take 0 ; :: according to SEQ_4:def 2 :: thesis: for b₁ being set holds
( not b₁ in Y or 0 <= b₁ )
let r be real number ; :: 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 D' & r = f . c ) by FUNCT_2:116;
hence 0 <= r by A2, Th9; :: thesis: verum

end;

hence dist_min A,D <= dist_min A,C by A1, A2, A3, A4, A5, A6, A7, A8, A9, RELAT_1:156, SEQ_4:64; :: thesis: verum