take {{{} }} ; :: thesis: ( not {{{} }} is empty & {{{} }} is with_non-empty_elements )
thus not {{{} }} is empty ; :: thesis: {{{} }} is with_non-empty_elements
assume {} in {{{} }} ; :: according to SETFAM_1:def 9 :: thesis: contradiction
hence contradiction by TARSKI:def 1; :: thesis: verum