let A, B be non empty compact Subset of REAL ; :: thesis: dist A,B >= 0
set X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } ;
consider r0 being set such that
A1: r0 in A by XBOOLE_0:def 1;
consider s0 being set such that
A2: s0 in B by XBOOLE_0:def 1;
( r0 is Real & s0 is Real ) by A1, A2;
then reconsider r0 = r0, s0 = s0 as real number ;
A3: abs (r0 - s0) in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } by A1, A2;
{ (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 non empty Subset of REAL by A3;
A4: dist A,B = lower_bound X by Def2;
for t being real number st t in X holds
t >= 0

proof

let t be real number ; :: thesis: ( t in X implies t >= 0 )
assume t in X ; :: thesis: t >= 0
then ex r, s being Real st
( t = abs (r - s) & r in A & s in B ) ;
hence t >= 0 by COMPLEX1:132; :: thesis: verum

end;

hence dist A,B >= 0 by A4, SEQ_4:60; :: thesis: verum