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

proof

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;

hence contradiction by A1, Def4; :: thesis: verum