theorem Th25: :: MEASUR11:31

for X being set
for Y being non empty set
for p being set
for F being SetSequence of [:X,Y:]
for Fy being SetSequence of Y st ( for n being Nat holds Fy . n = X-section ((F . n),p) ) holds
X-section ((meet (rng F)),p) = meet (rng Fy)