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

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

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

proof

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

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