let x be object ; :: thesis: for X being set
for B being SetSequence of X
for n being Nat holds
( x in (inferior_setsequence B) . n iff for k being Nat holds x in B . (n + k) )
let X be set ; :: thesis: for B being SetSequence of X
for n being Nat holds
( x in (inferior_setsequence B) . n iff for k being Nat holds x in B . (n + k) )
let B be SetSequence of X; :: thesis: for n being Nat holds
( x in (inferior_setsequence B) . n iff for k being Nat holds x in B . (n + k) )
let n be Nat; :: thesis: ( x in (inferior_setsequence B) . n iff for k being Nat holds x in B . (n + k) )
reconsider nn = n as Nat ;
set Y = { (B . k) where k is Nat : nn <= k } ;
A1: (inferior_setsequence B) . n = meet { (B . k) where k is Nat : n <= k } by Def2;

A2: now :: thesis: ( x in (inferior_setsequence B) . n implies for k being Nat holds x in B . (n + k) )

assume A3: x in (inferior_setsequence B) . n ; :: thesis: for k being Nat holds x in B . (n + k)

now :: thesis: for k being Nat holds x in B . (n + k)

let k be Nat; :: thesis: x in B . (n + k)
B . (n + k) in { (B . k) where k is Nat : nn <= k } by Th1;
hence x in B . (n + k) by A1, A3, SETFAM_1:def 1; :: thesis: verum

end;

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

end;

A4: { (B . k) where k is Nat : nn <= k } <> {} by Th1;

now :: thesis: ( ( for k being Nat holds x in B . (n + k) ) implies x in (inferior_setsequence B) . n )

assume for k being 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 Nat : nn <= k } holds
x in Z by Th3;
hence x in (inferior_setsequence B) . n by A1, A4, SETFAM_1:def 1; :: thesis: verum

end;

hence ( x in (inferior_setsequence B) . n iff for k being Nat holds x in B . (n + k) ) by A2; :: thesis: verum