( 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