for A being non empty Subset of ExtREAL
for r being ExtReal st r < sup A holds
ex s being Element of ExtREAL st
( s in A & r < s )