:: deftheorem defines lambda CAT_4:def 11 :
for C being Cartesian_category
for a being Object of C holds lambda a = pr2 (([1] C),a);