theorem :: SETLIM_1:26

for n being Nat
for X being set
for B being SetSequence of X holds Intersection B c= (inferior_setsequence B) . n