let P be non empty POSet_set; :: thesis: for o1, o2 being Object of (POSAltCat P)
for A, B being Element of P st o1 = A & o2 = B holds
<^o1,o2^> c= Funcs ( the carrier of A, the carrier of B)
let o1, o2 be Object of (POSAltCat P); :: thesis: for A, B being Element of P st o1 = A & o2 = B holds
<^o1,o2^> c= Funcs ( the carrier of A, the carrier of B)
let A, B be Element of P; :: thesis: ( o1 = A & o2 = B implies <^o1,o2^> c= Funcs ( the carrier of A, the carrier of B) )
assume A1: ( o1 = A & o2 = B ) ; :: thesis: <^o1,o2^> c= Funcs ( the carrier of A, the carrier of B)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in <^o1,o2^> or x in Funcs ( the carrier of A, the carrier of B) )
assume x in <^o1,o2^> ; :: thesis: x in Funcs ( the carrier of A, the carrier of B)
then x in MonFuncs (A,B) by A1, Def9;
then ex f being Function of A,B st
( f = x & f in Funcs ( the carrier of A, the carrier of B) & f is monotone ) by Def6;
hence x in Funcs ( the carrier of A, the carrier of B) ; :: thesis: verum