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

proof

let x be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( x in A implies x <= r )
assume x in A ; :: thesis: x <= r
hence x <= r by A2; :: thesis: verum

end;

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