let n be Nat; :: thesis: for X being set

for B being SetSequence of X st B is V55() holds

(superior_setsequence B) . n = B . n

let X be set ; :: thesis: for B being SetSequence of X st B is V55() holds

(superior_setsequence B) . n = B . n

let B be SetSequence of X; :: thesis: ( B is V55() implies (superior_setsequence B) . n = B . n )

assume B is V55() ; :: thesis: (superior_setsequence B) . n = B . n

then ((superior_setsequence B) . (n + 1)) \/ (B . n) = B . n by Th47, XBOOLE_1:12;

hence (superior_setsequence B) . n = B . n by Th22; :: thesis: verum

for B being SetSequence of X st B is V55() holds

(superior_setsequence B) . n = B . n

let X be set ; :: thesis: for B being SetSequence of X st B is V55() holds

(superior_setsequence B) . n = B . n

let B be SetSequence of X; :: thesis: ( B is V55() implies (superior_setsequence B) . n = B . n )

assume B is V55() ; :: thesis: (superior_setsequence B) . n = B . n

then ((superior_setsequence B) . (n + 1)) \/ (B . n) = B . n by Th47, XBOOLE_1:12;

hence (superior_setsequence B) . n = B . n by Th22; :: thesis: verum