let a, b be set ; :: thesis: not 1 = [a,b]
assume A1: 1 = [a,b] ; :: thesis: contradiction
{a} in {{a,b},{a}} by TARSKI:def 2;
hence contradiction by A1, ORDINAL3:15, TARSKI:def 1; :: thesis: verum