A class is called set if there exists another class that contains it. Otherwise it is called proper class, i.e. a class A with ¬set A is proper. Theorems UnivCl_intro and UnivCl_elim show that a class is a set, if and only if it is an element of UnivCl.