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