set Y = { |.(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

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;

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