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

A3: Y0 is bounded_below

|.(r - s).| in Y0 by A1, A2;

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

|.(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

then reconsider Y0 = { |.(r - s).| where r, s is Real : ( r in A & s in B ) } as Subset of REAL ;
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: Y0 is bounded_below

proof

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

|.(r - s).| in Y0 by A1, A2;

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