theorem Th9: :: EXCHSORT:9

for f being Function st f is segmental holds
for a, b, c being Ordinal st a c= b & b c= c & a in dom f & c in dom f holds
b in dom f