let x be ExtReal; :: thesis: x is LowerBound of {}

let y be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( y in {} implies x <= y )

thus ( y in {} implies x <= y ) ; :: thesis: verum

let y be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( y in {} implies x <= y )

thus ( y in {} implies x <= y ) ; :: thesis: verum