theorem Th3: :: SETLIM_1:3

for n being Nat
for x being object
for Y being set
for f being sequence of Y holds
( ( for k1 being Nat holds x in f . (n + k1) ) iff for Z being set st Z in { (f . k2) where k2 is Nat : n <= k2 } holds
x in Z )