theorem Th3: :: KURATO_0:3

for X being set
for F being SetSequence of X
for x being object holds
( x in meet F iff for z being Nat holds x in F . z )