theorem :: ALTCAT_4:59

for C being category holds AllIso (AllCoretr C) = AllIso C