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 set such that
A3: s0 in D by XBOOLE_0:def 1;
set Y = { (abs (r - s)) where r, s is Element of REAL : ( r in C & s in D ) } ;
consider r0 being set such that
A4: r0 in C by XBOOLE_0:def 1;
A5: { (abs (r - s)) where r, s is Element of REAL : ( r in C & s in D ) } c= REAL

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { (abs (r - s)) where r, s is Element of REAL : ( r in C & s in D ) } or e in REAL )
assume e in { (abs (r - s)) where r, s is Element of REAL : ( r in C & s in D ) } ; :: thesis: e in REAL
then ex r, s being Real st
( e = abs (r - s) & r in C & s in D ) ;
hence e in REAL ; :: thesis: verum

end;

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

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } or e in REAL )
assume e in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } ; :: thesis: e in REAL
then ex r, s being Real st
( e = abs (r - s) & r in A & s in B ) ;
hence e in REAL ; :: thesis: verum

end;

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

proof

let x be set ; :: 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 = abs (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 ext-real number ; :: 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 = abs (r - s) & r in A & s in B ) ;
hence 0 <= r0 by COMPLEX1:132; :: thesis: verum

end;

A8: dist C,D = lower_bound Y by Def2;
dist A,B = lower_bound X by Def2;
hence dist A,B <= dist C,D by A7, A8, A6, SEQ_4:64; :: thesis: verum