take {{{}}} ; :: thesis: {{{}}} is with_non-empty_element
take {{}} ; :: according to SETFAM_1:def 10 :: thesis: {{}} in {{{}}}
thus {{}} in {{{}}} by TARSKI:def 1; :: thesis: verum