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) )
set Y = { (B . k) where k is Element of NAT : n <= k } ;
A1: (inferior_setsequence B) . n = meet { (B . k) where k is Element of NAT : n <= k } by Def2;

A2: now

assume A3: 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 Th1;
hence x in B . (n + k) by A1, A3, SETFAM_1:def 1; :: thesis: verum

end;

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

end;

A4: { (B . k) where k is Element of NAT : n <= k } <> {} by Th1;

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 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 Element of NAT holds x in B . (n + k) ) by A2; :: thesis: verum