theorem :: ALTCAT_4:55

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