let P be non empty POSet_set; :: thesis: for A, B being Element of P holds MonFuncs (A,B) c= Funcs (Carr P)
let A, B be Element of P; :: thesis: MonFuncs (A,B) c= Funcs (Carr P)
reconsider CA = the carrier of A, CB = the carrier of B as Element of Carr P by Def7;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in MonFuncs (A,B) or x in Funcs (Carr P) )
assume x in MonFuncs (A,B) ; :: thesis: x in Funcs (Carr P)
then A1: ex g being Function of A,B st
( x = g & g in Funcs ( the carrier of A, the carrier of B) & g is monotone ) by Def6;
Funcs (CA,CB) c= Funcs (Carr P) by ENS_1:2;
hence x in Funcs (Carr P) by A1; :: thesis: verum