theorem Lm9: :: FINANCE3:21

for MySigmaField, MySet being set
for A1 being SetSequence of MySet st MySet = {1,2,3,4} & rng A1 c= MySigmaField & MySigmaField = {{},{1,2,3,4}} & Intersection A1 <> {} holds
Intersection A1 in MySigmaField