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