theorem Th45: :: SETLIM_1:45

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