theorem Th50: :: SETLIM_1:50

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