theorem Th12: :: WAYBEL34:12

for C being non empty AltCatStr
for a, b, f being object st f in the Arrows of C . (a,b) holds
ex o1, o2 being Object of C st
( o1 = a & o2 = b & f in <^o1,o2^> & f is Morphism of o1,o2 )