theorem :: ALTCAT_4:54

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