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 8 :: thesis: contradiction
hence contradiction by TARSKI:def 1; :: thesis: verum