theorem :: ALTCAT_4:53

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