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

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