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