for o being Object of (AllEpi C)
for o9 being Object of C st o = o9 holds
idm o9 in <^o,o^> by Def2;
hence AllEpi C is id-inheriting by ALTCAT_2:def 14; :: thesis: verum