let X be set ; :: thesis: for S being non empty diff-closed Subset-Family of X holds {} in S
let S be non empty diff-closed Subset-Family of X; :: thesis: {} in S
consider A being object such that
A1: A in S by XBOOLE_0:def 1;
reconsider A = A as set by TARSKI:1;
A \ A in S by A1, FINSUB_1:def 3;
hence {} in S by XBOOLE_1:37; :: thesis: verum