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

proof

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;

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

proof

thus X0 c= Y0 :: according to XBOOLE_0:def 10 :: thesis: Y0 c= X0

proof

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;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Y0 or x in 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;

hence IT = lower_bound Y0 by A2; :: thesis: verum