theorem Th47: :: SETLIM_1:47

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