theorem :: ALTCAT_4:58

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