theorem Th25: :: COHSP_1:25

for f being c=-monotone Function
for a, b being set st b in dom f & a c= b & b is finite holds
for y being set st [a,y] in graph f holds
[b,y] in graph f