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