let n be Nat; :: thesis: for X being set
for B being SetSequence of X st B is non-descending holds
B . n c= (inferior_setsequence B) . (n + 1)
let X be set ; :: thesis: for B being SetSequence of X st B is non-descending holds
B . n c= (inferior_setsequence B) . (n + 1)
let B be SetSequence of X; :: thesis: ( B is non-descending implies B . n c= (inferior_setsequence B) . (n + 1) )
set Y = { (B . k) where k is Nat : n + 1 <= k } ;
assume A1: B is non-descending ; :: thesis: B . n c= (inferior_setsequence B) . (n + 1)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B . n or x in (inferior_setsequence B) . (n + 1) )
assume A2: x in B . n ; :: thesis: x in (inferior_setsequence B) . (n + 1)

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

let y be set ; :: thesis: ( y in { (B . k) where k is Nat : n + 1 <= k } implies x in y )
assume y in { (B . k) where k is Nat : n + 1 <= k } ; :: thesis: x in y
then consider k1 being Nat such that
A4: y = B . k1 and
A5: n + 1 <= k1 ;
n <= k1 by A5, NAT_1:13;
then B . n c= B . k1 by A1, PROB_1:def 5;
hence x in y by A2, A4; :: thesis: verum

end;

A6: { (B . k) where k is Nat : n + 1 <= k } <> {} by Th1;
(inferior_setsequence B) . (n + 1) = meet { (B . k) where k is Nat : n + 1 <= k } by Def2;
hence x in (inferior_setsequence B) . (n + 1) by A6, A3, SETFAM_1:def 1; :: thesis: verum