theorem Th40: :: SETLIM_1:40

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