take
{{}}
; :: thesis: ( not {{}} is empty & not {{}} is with_non-empty_elements )

thus not {{}} is empty ; :: thesis: not {{}} is with_non-empty_elements

thus {} in {{}} by TARSKI:def 1; :: according to SETFAM_1:def 8 :: thesis: verum

thus not {{}} is empty ; :: thesis: not {{}} is with_non-empty_elements

thus {} in {{}} by TARSKI:def 1; :: according to SETFAM_1:def 8 :: thesis: verum