theorem Th21: :: SETLIM_1:21

for X being set
for B being SetSequence of X
for n being Nat holds (inferior_setsequence B) . n = ((inferior_setsequence B) . (n + 1)) /\ (B . n)