theorem :: ALTCAT_4:47

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