:: deftheorem defines Delta CAT_4:def 16 :
for C being Cartesian_category
for a being Object of C holds Delta a = <:(id a),(id a):>;