let A, B be Subset of REAL; :: thesis: for r, s being Real st r in A & s in B holds
|.(r - s).| >= dist (A,B)
set Y = { |.(r - s).| where r, s is Real : ( r in A & s in B ) } ;
let r, s be Real; :: thesis: ( r in A & s in B implies |.(r - s).| >= dist (A,B) )
assume that
A1: r in A and
A2: s in B ; :: thesis: |.(r - s).| >= dist (A,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 Y0 = { |.(r - s).| where r, s is 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 ExtReal; :: 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 = |.(r - s).| & r in A & s in B ) ;
hence 0 <= r0 by COMPLEX1:46; :: thesis: verum

end;

A4: dist (A,B) = lower_bound Y0 by Def1;
|.(r - s).| in Y0 by A1, A2;
hence |.(r - s).| >= dist (A,B) by A4, A3, SEQ_4:def 2; :: thesis: verum