:: deftheorem Def3 defines AllRetr ALTCAT_4:def 3 :
for C being category
for b₂ being non empty transitive strict SubCatStr of C holds
( b₂ = AllRetr C iff ( the carrier of b₂ = the carrier of C & the Arrows of b₂ cc= the Arrows of C & ( for o1, o2 being Object of C
for m being Morphism of o1,o2 holds
( m in the Arrows of b₂ . (o1,o2) iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & m is retraction ) ) ) ) );