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

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