set Y = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } ;
{ (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } c= REAL

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } or e in REAL )
assume e in { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } ; :: thesis: e in REAL
then ex r, s being Element of REAL st
( e = abs (r - s) & r in A & s in B ) ;
hence e in REAL ; :: thesis: verum

end;

then reconsider Y0 = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } as Subset of REAL ;
take lower_bound Y0 ; :: thesis: ex X being Subset of REAL st
( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & lower_bound Y0 = lower_bound X )
thus ex X being Subset of REAL st
( X = { (abs (r - s)) where r, s is Element of REAL : ( r in A & s in B ) } & lower_bound Y0 = lower_bound X ) ; :: thesis: verum