theorem :: ALTCAT_4:48

for C being category st ( for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m is coretraction & <^o2,o1^> <> {} ) ) holds
AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) = AllCoretr C