let A be non empty Subset of ExtREAL; :: thesis: for r being R_eal st inf A < r holds
ex s being R_eal st
( s in A & s < r )
let r be R_eal; :: thesis: ( inf A < r implies ex s being R_eal st
( s in A & s < r ) )
assume A1: inf A < r ; :: thesis: ex s being R_eal st
( s in A & s < r )
assume A2: for s being R_eal st s in A holds
not s < r ; :: thesis: contradiction
r is LowerBound of A

proof

let x be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( not x in A or r <= x )
assume x in A ; :: thesis: r <= x
hence r <= x by A2; :: thesis: verum

end;

hence contradiction by A1, XXREAL_2:def 4; :: thesis: verum