theorem :: CLASSES5:56

for o, m being object
for c being Object of (1Cat (o,m)) holds c = o