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