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

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