theorem :: IDEAL_2:37
for A being non degenerated commutative Ring
for p being prime Ideal of A
for F being non empty FinSequence of PRIMARY (A,p) holds meet (rng F) in PRIMARY (A,p)