let x be object ; :: thesis:
let X be set ; :: thesis:
let B be SetSequence of X; :: thesis:
let n be Nat; :: thesis:
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:

assume A3: x in (inferior_setsequence B) . n ; :: thesis:

now :: thesis:

let k be Nat; :: thesis:
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:

end;

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

end;

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

now :: thesis:

assume for k being Nat holds x in B . (n + k) ; :: thesis:
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:

end;

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