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