let C be category; ( ( for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m is coretraction & <^o2,o1^> <> {} ) ) implies AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) = AllCoretr C )
assume A1:
for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m is coretraction & <^o2,o1^> <> {} )
; AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) = AllCoretr C
A2:
the carrier of (AllCoretr C) = the carrier of AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #)
by Def4;
A3:
the Arrows of (AllCoretr C) cc= the Arrows of C
by Def4;
hence
AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) = AllCoretr C
by A2, ALTCAT_2:25, PBOOLE:3; verum