for o being object of (AllMono C)
for o' being object of C st o = o' holds
idm o' in <^o,o^> by Def1;
hence AllMono C is id-inheriting by ALTCAT_2:def 14; :: thesis: verum