:: deftheorem Def5 defines AllIso ALTCAT_4:def 5 :
for C being category
for b₂ being non empty transitive strict SubCatStr of C holds
( b₂ = AllIso 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 iso ) ) ) ) );