theorem Th33: :: MEASUR11:39

for X being set
for Y being non empty set
for x being set
for E being SetSequence of [:X,Y:]
for G being SetSequence of Y st E is non-descending & ( for n being Nat holds G . n = X-section ((E . n),x) ) holds
G is non-descending