take F = {} ; :: thesis: ( F is c=-monotone & F is Function-yielding )
for a, b being set st a in dom F & b in dom F & a c= b holds
F . a c= F . b ;
hence ( F is c=-monotone & F is Function-yielding ) by COHSP_1:def 11; :: thesis: verum