let G be non empty subset-closed set ; :: thesis: {} in G
consider z being set such that
A2: z in G by XBOOLE_0:def 1;
{} c= z by XBOOLE_1:2;
hence {} in G by A2, CLASSES1:def 1; :: thesis: verum