let n be Element of 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) )
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 . k) where k is Element of NAT : n + 1 <= k } <> {} by Th5;
assume A01: B is non-descending ; :: thesis: B . n c= (inferior_setsequence B) . (n + 1)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B . n or x in (inferior_setsequence B) . (n + 1) )
assume B00: x in B . n ; :: thesis: x in (inferior_setsequence B) . (n + 1)

now

let y be set ; :: thesis: ( y in { (B . k) where k is Element of NAT : n + 1 <= k } implies x in y )
assume y in { (B . k) where k is Element of NAT : n + 1 <= k } ; :: thesis: x in y
then consider k1 being Element of NAT such that
C00: ( y = B . k1 & n + 1 <= k1 ) ;
n <= k1 by C00, NAT_1:13;
then B . n c= B . k1 by A01, PROB_1:def 7;
hence x in y by B00, C00; :: thesis: verum

end;

hence x in (inferior_setsequence B) . (n + 1) by A00, AA0, SETFAM_1:def 1; :: thesis: verum