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