let x be ext-real number ; :: thesis: x is LowerBound of {}
let y be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( y in {} implies x <= y )
thus ( y in {} implies x <= y ) ; :: thesis: verum