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