theorem :: ALTCAT_4:56

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