let x, y be ExtReal; :: thesis: for z being UpperBound of {x,y} holds y <= z

let z be UpperBound of {x,y}; :: thesis: y <= z

y in {x,y} by TARSKI:def 2;

hence y <= z by Def1; :: thesis: verum

let z be UpperBound of {x,y}; :: thesis: y <= z

y in {x,y} by TARSKI:def 2;

hence y <= z by Def1; :: thesis: verum