theorem :: ALTCAT_4:57

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