let x, y be ExtReal; :: thesis: x is LowerBound of [.x,y.[
let z be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( z in [.x,y.[ implies x <= z )
assume z in [.x,y.[ ; :: thesis: x <= z
hence x <= z by XXREAL_1:3; :: thesis: verum