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 )
A00: (inferior_setsequence B) . (n + 1) = meet { (B . k) where k is Element of NAT : n + 1 <= k } by def2;
set Y = { (B . k) where k is Element of NAT : n + 1 <= k } ;
AA0: B . (n + 1) in { (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 A02: B . (n + 1) c= B . n by PROB_2:14;

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 AA0, SETFAM_1:def 1;
hence x in B . n by A02; :: thesis: verum

end;

hence (inferior_setsequence B) . (n + 1) c= B . n by A00, TARSKI:def 3; :: thesis: verum