let A, B be Subset of REAL ; :: thesis: for r, s being real number st r in A & s in B holds
abs (r - s) >= dist A,B
set Y = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } ;
let r, s be real number ; :: thesis: ( r in A & s in B implies abs (r - s) >= dist A,B )
assume that
A1: r in A and
A2: s in B ; :: thesis: abs (r - s) >= dist A,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 Y0 = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } as Subset of REAL ;
A3: Y0 is bounded_below

proof

take 0 ; :: according to XXREAL_2:def 9 :: thesis: 0 is LowerBound of Y0
let r0 be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( not r0 in Y0 or 0 <= r0 )
assume r0 in Y0 ; :: 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;

A4: dist A,B = lower_bound Y0 by Def2;
abs (r - s) in Y0 by A1, A2;
hence abs (r - s) >= dist A,B by A4, A3, SEQ_4:def 5; :: thesis: verum