The universal class. It contains all the sets, as UnivCl_intro and UnivCl_elim show. But it must be distinguished from the class universe, which is the entire universe of discourse of the logical system. As empty_set_is_least and UnivCl_is_greatest show, the empty set and the universal class are the least and greatest element of the class universe. Thus, all classes are subclasses of UnivCl.