let x, y be ExtReal; :: thesis: for z being LowerBound of {x,y} holds z <= y
let z be LowerBound of {x,y}; :: thesis: z <= y
y in {x,y} by TARSKI:def 2;
hence z <= y by Def2; :: thesis: verum