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

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

(superior_setsequence B) . (n + 1) c= B . n

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

(superior_setsequence B) . (n + 1) c= B . n

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

assume A1: B is V55() ; :: thesis: (superior_setsequence B) . (n + 1) c= B . n

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (superior_setsequence B) . (n + 1) or x in B . n )

assume x in (superior_setsequence B) . (n + 1) ; :: thesis: x in B . n

then consider k being Nat such that

A2: x in B . ((n + 1) + k) by Th20;

n + 1 <= (n + 1) + k by NAT_1:11;

then n <= (n + 1) + k by NAT_1:13;

then B . ((n + 1) + k) c= B . n by A1, PROB_1:def 4;

hence x in B . n by A2; :: thesis: verum

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

(superior_setsequence B) . (n + 1) c= B . n

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

(superior_setsequence B) . (n + 1) c= B . n

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

assume A1: B is V55() ; :: thesis: (superior_setsequence B) . (n + 1) c= B . n

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (superior_setsequence B) . (n + 1) or x in B . n )

assume x in (superior_setsequence B) . (n + 1) ; :: thesis: x in B . n

then consider k being Nat such that

A2: x in B . ((n + 1) + k) by Th20;

n + 1 <= (n + 1) + k by NAT_1:11;

then n <= (n + 1) + k by NAT_1:13;

then B . ((n + 1) + k) c= B . n by A1, PROB_1:def 4;

hence x in B . n by A2; :: thesis: verum