theorem Th12: :: PROB_3:12

for n being Nat
for X being set
for A1 being SetSequence of X
for x being object holds
( x in (Partial_Intersection A1) . n iff for k being Nat st k <= n holds
x in A1 . k )