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 that
A1: b in dom f and
A2: a c= b and
A3: 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 A4: [a,y] in graph f ; :: thesis: [b,y] in graph f
then a in dom f by Th24;
then A5: f . a c= f . b by A1, A2, Def11;
y in f . a by A4, Th24;
hence [b,y] in graph f by A1, A3, A5, Th24; :: thesis: verum