:: deftheorem defines Alpha' CAT_4:def 18 :
for C being Cartesian_category
for a, b, c being Object of C holds Alpha' (a,b,c) = <:<:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((pr2 (b,c)) * (pr2 (a,(b [x] c)))):>;