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 consider f being Function of A,B such that
A2: ( f = x & f in Funcs the carrier of A,the carrier of B & f is monotone ) by Def6;
thus x in Funcs the carrier of A,the carrier of B by A2; :: thesis: verum