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

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