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