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