take {{{}}} ; :: thesis: not {{{}}} is empty-membered
take {{}} ; :: according to SETFAM_1:def 10 :: thesis: {{}} in {{{}}}
thus {{}} in {{{}}} by TARSKI:def 1; :: thesis: verum