:: deftheorem Def5 defines superior_realsequence RINFSUP1:def 5 :
for seq, b₂ being Real_Sequence holds
( b₂ = superior_realsequence seq iff for n being Nat
for Y being Subset of REAL st Y = { (seq . k) where k is Nat : n <= k } holds
b₂ . n = upper_bound Y );