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