theorem Th13: :: PROB_1:13

for X being set
for A1 being SetSequence of X
for x being object holds
( x in Intersection A1 iff for n being Nat holds x in A1 . n )