theorem Th19: :: SETLIM_1:19

for x being object
for X being set
for B being SetSequence of X
for n being Nat holds
( x in (inferior_setsequence B) . n iff for k being Nat holds x in B . (n + k) )