theorem Th46: :: SETLIM_1:46

for X being set
for B being SetSequence of X st B is non-descending holds
inferior_setsequence B = B