let G be non empty subset-closed set ; :: thesis: {} in G
consider z being object such that
A1: z in G by XBOOLE_0:def 1;
reconsider z = z as set by TARSKI:1;
{} c= z ;
hence {} in G by A1, CLASSES1:def 1; :: thesis: verum