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

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

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

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

consider s0 being object such that
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;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

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

dist (A,B) = lower_bound X
by Def1;
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;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

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