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 set ; :: 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