set o = the Object of C;
take ObCat the Object of C ; :: thesis: ( ObCat the Object of C is transitive & not ObCat the Object of C is empty & ObCat the Object of C is strict )
thus ( ObCat the Object of C is transitive & not ObCat the Object of C is empty & ObCat the Object of C is strict ) ; :: thesis: verum