let IT be Real; :: thesis: for A, B being Subset of REAL st ex X being Subset of REAL st

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

ex X being Subset of REAL st

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

let A, B be Subset of REAL; :: thesis: ( ex X being Subset of REAL st

( X = { |.(r - s).| where r, s is Real : ( r in A & s in B ) } & IT = lower_bound X ) implies ex X being Subset of REAL st

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

given X0 being Subset of REAL such that A1: X0 = { |.(r - s).| where r, s is Real : ( r in A & s in B ) } and

A2: IT = lower_bound X0 ; :: thesis: ex X being Subset of REAL st

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

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

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

take Y0 ; :: thesis: ( Y0 = { |.(r - s).| where r, s is Real : ( r in B & s in A ) } & IT = lower_bound Y0 )

thus Y0 = { |.(r - s).| where r, s is Real : ( r in B & s in A ) } ; :: thesis: IT = lower_bound Y0

X0 = Y0

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

ex X being Subset of REAL st

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

let A, B be Subset of REAL; :: thesis: ( ex X being Subset of REAL st

( X = { |.(r - s).| where r, s is Real : ( r in A & s in B ) } & IT = lower_bound X ) implies ex X being Subset of REAL st

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

given X0 being Subset of REAL such that A1: X0 = { |.(r - s).| where r, s is Real : ( r in A & s in B ) } and

A2: IT = lower_bound X0 ; :: thesis: ex X being Subset of REAL st

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

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

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

proof

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

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

then ex r, s being Real st

( e = |.(r - s).| & r in B & s in A ) ;

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

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

then ex r, s being Real st

( e = |.(r - s).| & r in B & s in A ) ;

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

take Y0 ; :: thesis: ( Y0 = { |.(r - s).| where r, s is Real : ( r in B & s in A ) } & IT = lower_bound Y0 )

thus Y0 = { |.(r - s).| where r, s is Real : ( r in B & s in A ) } ; :: thesis: IT = lower_bound Y0

X0 = Y0

proof

hence
IT = lower_bound Y0
by A2; :: thesis: verum
thus
X0 c= Y0
:: according to XBOOLE_0:def 10 :: thesis: Y0 c= X0

assume x in Y0 ; :: thesis: x in X0

then consider r, s being Real such that

A6: x = |.(r - s).| and

A7: r in B and

A8: s in A ;

x = |.(s - r).| by A6, UNIFORM1:11;

hence x in X0 by A1, A7, A8; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Y0 or x in X0 )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X0 or x in Y0 )

assume x in X0 ; :: thesis: x in Y0

then consider r, s being Real such that

A3: x = |.(r - s).| and

A4: r in A and

A5: s in B by A1;

x = |.(s - r).| by A3, UNIFORM1:11;

hence x in Y0 by A4, A5; :: thesis: verum

end;assume x in X0 ; :: thesis: x in Y0

then consider r, s being Real such that

A3: x = |.(r - s).| and

A4: r in A and

A5: s in B by A1;

x = |.(s - r).| by A3, UNIFORM1:11;

hence x in Y0 by A4, A5; :: thesis: verum

assume x in Y0 ; :: thesis: x in X0

then consider r, s being Real such that

A6: x = |.(r - s).| and

A7: r in B and

A8: s in A ;

x = |.(s - r).| by A6, UNIFORM1:11;

hence x in X0 by A1, A7, A8; :: thesis: verum