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