theorem Th36: :: MEASUR11:42

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