let A be non empty Subset of ExtREAL; :: thesis: for r being Element of ExtREAL st inf A < r holds

ex s being Element of ExtREAL st

( s in A & s < r )

let r be Element of ExtREAL ; :: thesis: ( inf A < r implies ex s being Element of ExtREAL st

( s in A & s < r ) )

assume A1: inf A < r ; :: thesis: ex s being Element of ExtREAL st

( s in A & s < r )

assume A2: for s being Element of ExtREAL st s in A holds

not s < r ; :: thesis: contradiction

r is LowerBound of A

ex s being Element of ExtREAL st

( s in A & s < r )

let r be Element of ExtREAL ; :: thesis: ( inf A < r implies ex s being Element of ExtREAL st

( s in A & s < r ) )

assume A1: inf A < r ; :: thesis: ex s being Element of ExtREAL st

( s in A & s < r )

assume A2: for s being Element of ExtREAL st s in A holds

not s < r ; :: thesis: contradiction

r is LowerBound of A

proof

hence
contradiction
by A1, Def4; :: thesis: verum
let x be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( x in A implies r <= x )

thus ( x in A implies r <= x ) by A2; :: thesis: verum

end;thus ( x in A implies r <= x ) by A2; :: thesis: verum