let n be Element of NAT ; :: thesis: for X, x being set
for B being SetSequence of X holds
( x in (inferior_setsequence B) . n iff for k being Element of NAT holds x in B . (n + k) )
let X, x be set ; :: thesis: for B being SetSequence of X holds
( x in (inferior_setsequence B) . n iff for k being Element of NAT holds x in B . (n + k) )
let B be SetSequence of X; :: thesis: ( x in (inferior_setsequence B) . n iff for k being Element of NAT holds x in B . (n + k) )
A0: (inferior_setsequence B) . n = meet { (B . k) where k is Element of NAT : n <= k } by def2;
set Y = { (B . k) where k is Element of NAT : n <= k } ;
B: { (B . k) where k is Element of NAT : n <= k } <> {} by Th5;

A00: now

assume B1: x in (inferior_setsequence B) . n ; :: thesis: for k being Element of NAT holds x in B . (n + k)

now

let k be Element of NAT ; :: thesis: x in B . (n + k)
B . (n + k) in { (B . k) where k is Element of NAT : n <= k } by Th5;
hence x in B . (n + k) by A0, B1, SETFAM_1:def 1; :: thesis: verum

end;

hence for k being Element of NAT holds x in B . (n + k) ; :: thesis: verum

end;

now

assume for k being Element of NAT holds x in B . (n + k) ; :: thesis: x in (inferior_setsequence B) . n
then for Z being set st Z in { (B . k) where k is Element of NAT : n <= k } holds
x in Z by Th7;
hence x in (inferior_setsequence B) . n by A0, B, SETFAM_1:def 1; :: thesis: verum

end;

hence ( x in (inferior_setsequence B) . n iff for k being Element of NAT holds x in B . (n + k) ) by A00; :: thesis: verum