theorem Th44: :: SETLIM_1:44

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