let X be set ; :: thesis: for B being SetSequence of X
for n being Nat st B is non-ascending holds
(inferior_setsequence B) . (n + 1) c= B . n
let B be SetSequence of X; :: thesis: for n being Nat st B is non-ascending holds
(inferior_setsequence B) . (n + 1) c= B . n
let n be Nat; :: thesis: ( B is non-ascending implies (inferior_setsequence B) . (n + 1) c= B . n )
set Y = { (B . k) where k is Nat : n + 1 <= k } ;
assume B is non-ascending ; :: thesis: (inferior_setsequence B) . (n + 1) c= B . n
then A1: B . (n + 1) c= B . n by PROB_2:6;
A2: B . (n + 1) in { (B . k) where k is Nat : n + 1 <= k } ;

A3: now :: thesis: for x being object st x in meet { (B . k) where k is Nat : n + 1 <= k } holds
x in B . n

let x be object ; :: thesis: ( x in meet { (B . k) where k is Nat : n + 1 <= k } implies x in B . n )
assume x in meet { (B . k) where k is Nat : n + 1 <= k } ; :: thesis: x in B . n
then x in B . (n + 1) by A2, SETFAM_1:def 1;
hence x in B . n by A1; :: thesis: verum

end;

(inferior_setsequence B) . (n + 1) = meet { (B . k) where k is Nat : n + 1 <= k } by Def2;
hence (inferior_setsequence B) . (n + 1) c= B . n by A3; :: thesis: verum