let T be set ; for F being SetSequence of T
for x being object st F is V52() & ex k being Nat st
for n being Nat st n > k holds
x in F . n holds
x in meet F
let F be SetSequence of T; for x being object st F is V52() & ex k being Nat st
for n being Nat st n > k holds
x in F . n holds
x in meet F
let x be object ; ( F is V52() & ex k being Nat st
for n being Nat st n > k holds
x in F . n implies x in meet F )
assume A1:
F is V52()
; ( for k being Nat ex n being Nat st
( n > k & not x in F . n ) or x in meet F )
given k being Nat such that A2:
for n being Nat st n > k holds
x in F . n
; x in meet F
k + 1 > k
by NAT_1:13;
then A3:
x in F . (k + 1)
by A2;
assume
not x in meet F
; contradiction
then
not x in meet (rng F)
by FUNCT_6:def 4;
then consider Y being set such that
A4:
Y in rng F
and
A5:
not x in Y
by SETFAM_1:def 1;
consider y being object such that
A6:
y in dom F
and
A7:
Y = F . y
by A4, FUNCT_1:def 3;
reconsider y = y as Nat by A6;