let D be non empty set ; :: thesis: not {} in BOOL D
assume {} in BOOL D ; :: thesis: contradiction
then not {} in {{}} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis: verum