let A, B be Subset of REAL; :: thesis: for C, D being non empty Subset of REAL st C c= A & D c= B holds
dist (A,B) <= dist (C,D)
let C, D be non empty Subset of REAL; :: thesis: ( C c= A & D c= B implies dist (A,B) <= dist (C,D) )
assume that
A1: C c= A and
A2: D c= B ; :: thesis: dist (A,B) <= dist (C,D)
consider s0 being object such that
A3: s0 in D by XBOOLE_0:def 1;
set Y = { |.(r - s).| where r, s is Real : ( r in C & s in D ) } ;
consider r0 being object such that
A4: r0 in C by XBOOLE_0:def 1;
A5: { |.(r - s).| where r, s is Real : ( r in C & s in D ) } c= REAL

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { |.(r - s).| where r, s is Real : ( r in C & s in D ) } or e in REAL )
assume e in { |.(r - s).| where r, s is Real : ( r in C & s in D ) } ; :: thesis: e in REAL
then ex r, s being Real st
( e = |.(r - s).| & r in C & s in D ) ;
hence e in REAL by XREAL_0:def 1; :: thesis: verum

end;

reconsider r0 = r0, s0 = s0 as Real by A4, A3;
|.(r0 - s0).| in { |.(r - s).| where r, s is Real : ( r in C & s in D ) } by A4, A3;
then reconsider Y = { |.(r - s).| where r, s is Real : ( r in C & s in D ) } as non empty Subset of REAL by A5;
set X = { |.(r - s).| where r, s is Real : ( r in A & s in B ) } ;
{ |.(r - s).| where r, s is Real : ( r in A & s in B ) } c= REAL

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { |.(r - s).| where r, s is Real : ( r in A & s in B ) } or e in REAL )
assume e in { |.(r - s).| where r, s is Real : ( r in A & s in B ) } ; :: thesis: e in REAL
then ex r, s being Real st
( e = |.(r - s).| & r in A & s in B ) ;
hence e in REAL by XREAL_0:def 1; :: thesis: verum

end;

then reconsider X = { |.(r - s).| where r, s is Real : ( r in A & s in B ) } as Subset of REAL ;
A6: Y c= X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in X )
assume x in Y ; :: thesis: x in X
then ex r, s being Real st
( x = |.(r - s).| & r in C & s in D ) ;
hence x in X by A1, A2; :: thesis: verum

end;

A7: X is bounded_below

proof

take 0 ; :: according to XXREAL_2:def 9 :: thesis: 0 is LowerBound of X
let r0 be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not r0 in X or 0 <= r0 )
assume r0 in X ; :: thesis: 0 <= r0
then ex r, s being Real st
( r0 = |.(r - s).| & r in A & s in B ) ;
hence 0 <= r0 by COMPLEX1:46; :: thesis: verum

end;

A8: dist (C,D) = lower_bound Y by Def1;
dist (A,B) = lower_bound X by Def1;
hence dist (A,B) <= dist (C,D) by A7, A8, A6, SEQ_4:47; :: thesis: verum