theorem Th51: :: SETLIM_1:51

for X being set
for B being SetSequence of X
for n being Nat st B is non-ascending holds
(inferior_setsequence B) . n = (inferior_setsequence B) . (n + 1)