theorem Th27: :: MEASUR11:33

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