theorem Th59: :: CLASSES5:57

for o, m being object
for c being Element of (1Cat (o,m)) holds
( c is Object of (1Cat (o,m)) & c = o & id c = m )