take {{},{{}}} ; :: thesis: not {{},{{}}} is trivial
take {} ; :: according to ZFMISC_1:def 10 :: thesis: ex y being set st
( {} in {{},{{}}} & y in {{},{{}}} & not {} = y )
take {{}} ; :: thesis: ( {} in {{},{{}}} & {{}} in {{},{{}}} & not {} = {{}} )
thus ( {} in {{},{{}}} & {{}} in {{},{{}}} ) by TARSKI:def 2; :: thesis: not {} = {{}}
{} in {{}} by TARSKI:def 1;
hence {} <> {{}} ; :: thesis: verum