:: deftheorem Def4 defines inferior_realsequence RINFSUP1:def 4 :
for seq, b₂ being Real_Sequence holds
( b₂ = inferior_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 = lower_bound Y );