Description: A theorem about the universal class. Inference associated with bj-abv (which is proved from fewer axioms). (Contributed by Stefan Allan, 9-Dec-2008)