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

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

hence
contradiction
by A1, Def3; :: thesis: verum
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;assume x in A ; :: thesis: x <= r

hence x <= r by A2; :: thesis: verum