let f be c=-monotone Function; :: thesis: 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
let a, b be set ; :: thesis: ( b in dom f & a c= b & b is finite implies for y being set st [a,y] in graph f holds
[b,y] in graph f )
assume A1: ( b in dom f & a c= b & b is finite ) ; :: thesis: for y being set st [a,y] in graph f holds
[b,y] in graph f
let y be set ; :: thesis: ( [a,y] in graph f implies [b,y] in graph f )
assume A2: [a,y] in graph f ; :: thesis: [b,y] in graph f
then a in dom f by Th25;
then ( y in f . a & f . a c= f . b ) by A1, A2, Def12, Th25;
hence [b,y] in graph f by A1, Th25; :: thesis: verum