let A, B be set ; :: thesis: not A in [:A,B:]
assume A in [:A,B:] ; :: thesis: contradiction
then consider x, y being object such that
A1: ( x in A & y in B & A = [x,y] ) by Th83;
reconsider x = x as set by TARSKI:1;
( x = {x} or x = {x,y} ) by A1, TARSKI:def 2;
then x in x by TARSKI:def 1, TARSKI:def 2;
hence contradiction ; :: thesis: verum