:: deftheorem Def6 defines inferior_realsequence RINFSUP2:def 6 :
for seq, b₂ being ExtREAL_sequence holds
( b₂ = inferior_realsequence seq iff for n being Nat ex Y being non empty Subset of ExtREAL st
( Y = { (seq . k) where k is Nat : n <= k } & b₂ . n = inf Y ) );