consider o being object of C;
take D = ObCat o; :: thesis: ( D is id-inheriting & D is transitive )
thus ( D is id-inheriting & D is transitive ) ; :: thesis: verum