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