( f in <^a,b^> & <^a,b^> c= MonFuncs (latt a),(latt b) ) by A1, Def4;
then ex g being Function of (latt a),(latt b) st
( f = g & g in Funcs the carrier of (latt a),the carrier of (latt b) & g is monotone ) by ORDERS_3:def 6;
hence f is monotone Function of (latt a),(latt b) ; :: thesis: verum