let X be set ; :: thesis: for B being SetSequence of X
for n being Nat st B is non-descending holds
(superior_setsequence B) . n = (superior_setsequence B) . (n + 1)
let B be SetSequence of X; :: thesis: for n being Nat st B is non-descending holds
(superior_setsequence B) . n = (superior_setsequence B) . (n + 1)
let n be Nat; :: thesis: ( B is non-descending implies (superior_setsequence B) . n = (superior_setsequence B) . (n + 1) )
assume B is non-descending ; :: thesis: (superior_setsequence B) . n = (superior_setsequence B) . (n + 1)
then ((superior_setsequence B) . (n + 1)) \/ (B . n) = (superior_setsequence B) . (n + 1) by Th40, XBOOLE_1:12;
hence (superior_setsequence B) . n = (superior_setsequence B) . (n + 1) by Th22; :: thesis: verum