:: deftheorem Def8 defines sup XXREAL_2:def 8 :
for X being ext-real-membered right_end set
for b₂ being ExtReal holds
( b₂ = sup X iff ( b₂ in X & ( for x being ExtReal st x in X holds
x <= b₂ ) ) );