let U be Universe; :: thesis: {} in U
consider x being Element of U;
{} c= x by XBOOLE_1:2;
hence {} in U by CLASSES1:def 1; :: thesis: verum