for X being ext-real-membered set
for x being ExtReal st ex y being ExtReal st
( y in X & x <= y ) holds
x <= sup X