let A, B be Subset of REAL; :: thesis: for C, D being non empty Subset of REAL st C c= A & D c= B holds

dist (A,B) <= dist (C,D)

let C, D be non empty Subset of REAL; :: thesis: ( C c= A & D c= B implies dist (A,B) <= dist (C,D) )

assume that

A1: C c= A and

A2: D c= B ; :: thesis: dist (A,B) <= dist (C,D)

consider s0 being object such that

A3: s0 in D by XBOOLE_0:def 1;

set Y = { |.(r - s).| where r, s is Real : ( r in C & s in D ) } ;

consider r0 being object such that

A4: r0 in C by XBOOLE_0:def 1;

A5: { |.(r - s).| where r, s is Real : ( r in C & s in D ) } c= REAL

|.(r0 - s0).| in { |.(r - s).| where r, s is Real : ( r in C & s in D ) } by A4, A3;

then reconsider Y = { |.(r - s).| where r, s is Real : ( r in C & s in D ) } as non empty Subset of REAL by A5;

set X = { |.(r - s).| where r, s is Real : ( r in A & s in B ) } ;

{ |.(r - s).| where r, s is Real : ( r in A & s in B ) } c= REAL

A6: Y c= X

dist (A,B) = lower_bound X by Def1;

hence dist (A,B) <= dist (C,D) by A7, A8, A6, SEQ_4:47; :: thesis: verum

dist (A,B) <= dist (C,D)

let C, D be non empty Subset of REAL; :: thesis: ( C c= A & D c= B implies dist (A,B) <= dist (C,D) )

assume that

A1: C c= A and

A2: D c= B ; :: thesis: dist (A,B) <= dist (C,D)

consider s0 being object such that

A3: s0 in D by XBOOLE_0:def 1;

set Y = { |.(r - s).| where r, s is Real : ( r in C & s in D ) } ;

consider r0 being object such that

A4: r0 in C by XBOOLE_0:def 1;

A5: { |.(r - s).| where r, s is Real : ( r in C & s in D ) } c= REAL

proof

reconsider r0 = r0, s0 = s0 as Real by A4, A3;
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { |.(r - s).| where r, s is Real : ( r in C & s in D ) } or e in REAL )

assume e in { |.(r - s).| where r, s is Real : ( r in C & s in D ) } ; :: thesis: e in REAL

then ex r, s being Real st

( e = |.(r - s).| & r in C & s in D ) ;

hence e in REAL by XREAL_0:def 1; :: thesis: verum

end;assume e in { |.(r - s).| where r, s is Real : ( r in C & s in D ) } ; :: thesis: e in REAL

then ex r, s being Real st

( e = |.(r - s).| & r in C & s in D ) ;

hence e in REAL by XREAL_0:def 1; :: thesis: verum

|.(r0 - s0).| in { |.(r - s).| where r, s is Real : ( r in C & s in D ) } by A4, A3;

then reconsider Y = { |.(r - s).| where r, s is Real : ( r in C & s in D ) } as non empty Subset of REAL by A5;

set X = { |.(r - s).| where r, s is Real : ( r in A & s in B ) } ;

{ |.(r - s).| where r, s is Real : ( r in A & s in B ) } c= REAL

proof

then reconsider X = { |.(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

A6: Y c= X

proof

A7:
X is bounded_below
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in X )

assume x in Y ; :: thesis: x in X

then ex r, s being Real st

( x = |.(r - s).| & r in C & s in D ) ;

hence x in X by A1, A2; :: thesis: verum

end;assume x in Y ; :: thesis: x in X

then ex r, s being Real st

( x = |.(r - s).| & r in C & s in D ) ;

hence x in X by A1, A2; :: thesis: verum

proof

A8:
dist (C,D) = lower_bound Y
by Def1;
take
0
; :: according to XXREAL_2:def 9 :: thesis: 0 is LowerBound of X

let r0 be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not r0 in X or 0 <= r0 )

assume r0 in X ; :: 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 X or 0 <= r0 )

assume r0 in X ; :: 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

dist (A,B) = lower_bound X by Def1;

hence dist (A,B) <= dist (C,D) by A7, A8, A6, SEQ_4:47; :: thesis: verum