theorem Th22: :: SETLIM_1:22

for X being set
for B being SetSequence of X
for n being Nat holds (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n)