let A, B be non empty compact Subset of REAL; :: thesis: dist (A,B) >= 0
set X = { |.(r - s).| where r, s is Real : ( r in A & s in B ) } ;
consider r0 being object such that
A1: r0 in A by XBOOLE_0:def 1;
A2: { |.(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;

consider s0 being object such that
A3: s0 in B by XBOOLE_0:def 1;
reconsider r0 = r0, s0 = s0 as Real by A1, A3;
|.(r0 - s0).| in { |.(r - s).| where r, s is Real : ( r in A & s in B ) } by A1, A3;
then reconsider X = { |.(r - s).| where r, s is Real : ( r in A & s in B ) } as non empty Subset of REAL by A2;
A4: for t being Real st t in X holds
t >= 0

proof

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

end;

dist (A,B) = lower_bound X by Def1;
hence dist (A,B) >= 0 by A4, SEQ_4:43; :: thesis: verum