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;

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) )

A4:
{ (B . k) where k is Nat : nn <= k } <> {}
by Th1;assume A3:
x in (inferior_setsequence B) . n
; :: thesis: for k being Nat holds x in B . (n + k)

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

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

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

hence
( x in (inferior_setsequence B) . n iff for k being Nat holds x in B . (n + k) )
by A2; :: thesis: verumassume
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;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