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

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