let U be Universe; :: thesis: {} in U
{} c= the Element of U ;
hence {} in U by CLASSES1:def 1; :: thesis: verum