let n be Element of NAT ; :: thesis: for X being set
for B being SetSequence of X st B is non-ascending holds
(inferior_setsequence B) . (n + 1) c= B . n
let X be set ; :: thesis: for B being SetSequence of X st B is non-ascending holds
(inferior_setsequence B) . (n + 1) c= B . n
let B be SetSequence of X; :: thesis: ( B is non-ascending implies (inferior_setsequence B) . (n + 1) c= B . n )
set Y = { (B . k) where k is Element of 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 Element of NAT : n + 1 <= k } ;

A3: now

let x be set ; :: thesis: ( x in meet { (B . k) where k is Element of NAT : n + 1 <= k } implies x in B . n )
assume x in meet { (B . k) where k is Element of 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 Element of NAT : n + 1 <= k } by Def2;
hence (inferior_setsequence B) . (n + 1) c= B . n by A3, TARSKI:def 3; :: thesis: verum