:: deftheorem Def1 defines upper_bound SEQ_4:def 1 :
for X being real-membered set st not X is empty & X is bounded_above holds
for b₂ being Real holds
( b₂ = upper_bound X iff ( ( for r being Real st r in X holds
r <= b₂ ) & ( for s being Real st 0 < s holds
ex r being Real st
( r in X & b₂ - s < r ) ) ) );