This is the meta-level predicate for the 'rigid' classes of a theory (cf. Wiggins, 1980: within a given theory, if A is an instance of a !type class C in a conceivable situation s1, there is no conceivable s2 different from s1 in which A is not an instance of C). A type class is also countable (there is a part of something belonging to the class c which does not belong to c as well; in other terms, an instance of a !type class can be internally dishomogeneous). The first axiom implements rigidity, while the second implements countability.
(Inherited-Slot-Value Type The-Archetype Type)
(=> (Type ?Self)
(And (Exists
(?Sit1)
(And (Situation ?Sit1)
(Context-Of ?Sit1 ?Self)
(Forall
(?X)
(=> (Instance-Of ?X ?Self)
(Not (Exists
(?Sit2)
(And (Situation ?Sit2)
(Context-Of ?Sit2 ?Self)
(Context-Of ?Sit2 ?X)
(Different ?Sit2 ?Sit1)
(Exists
(?A)
(And (Not (Instance-Of
?X
?Self))
(Holds-At ?Sit2 ?A))))))))))
(Forall (?Y)
(=> (Instance-Of ?Y ?Self)
(Exists (?Z ?Dishomog)
(And (Instance-Of ?Z ?Dishomog)
(Part-Of ?Z ?Y)
(Conceptually-Different ?Self
?Dishomog)))))))