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:2; :: thesis: verum

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:2; :: thesis: verum