theorem Th20: :: SETLIM_1:20

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