let X be set ; :: thesis: for B being SetSequence of X
for n being Nat st B is V56() holds
(superior_setsequence B) . n = (superior_setsequence B) . (n + 1)
let B be SetSequence of X; :: thesis: for n being Nat st B is V56() holds
(superior_setsequence B) . n = (superior_setsequence B) . (n + 1)
let n be Nat; :: thesis: ( B is V56() implies (superior_setsequence B) . n = (superior_setsequence B) . (n + 1) )
assume B is V56() ; :: 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