let P be non empty POSet_set; 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); 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; ( o1 = A & o2 = B implies <^o1,o2^> c= Funcs ( the carrier of A, the carrier of B) )
assume A1:
( o1 = A & o2 = B )
; <^o1,o2^> c= Funcs ( the carrier of A, the carrier of B)
let x be object ; TARSKI:def 3 ( not x in <^o1,o2^> or x in Funcs ( the carrier of A, the carrier of B) )
assume
x in <^o1,o2^>
; 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)
; verum