let S be Subset-Family of X; :: thesis: ( not S is empty & S is diff-closed implies S is with_empty_element )
assume A0: ( not S is empty & S is diff-closed ) ; :: thesis: S is with_empty_element
then consider A being object such that
A1: A in S ;
reconsider A = A as set by TARSKI:1;
A \ A in S by A0, A1;
hence S is with_empty_element by XBOOLE_1:37; :: thesis: verum