:: deftheorem Def6 defines right_end XXREAL_2:def 6 :
for X being ext-real-membered set holds
( X is right_end iff sup X in X );