let x, y be ExtReal; :: thesis: ( y <= x implies y is LowerBound of {x,y} )
assume A1: y <= x ; :: thesis: y is LowerBound of {x,y}
let z be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( z in {x,y} implies y <= z )
assume z in {x,y} ; :: thesis: y <= z
hence y <= z by A1, TARSKI:def 2; :: thesis: verum