let X be set ; :: thesis: ( X c= [:X,X:] implies X = {} )
assume A1: X c= [:X,X:] ; :: thesis: X = {}
assume X <> {} ; :: thesis: contradiction
then consider z being set such that
A2: z in X by XBOOLE_0:7;
z in X \/ (union X) by A2, XBOOLE_0:def 3;
then consider Y being set such that
A3: Y in X \/ (union X) and
A4: for x being set holds
( not x in X \/ (union X) or not x in Y ) by TARSKI:7;

now

assume A5: Y in X ; :: thesis: contradiction
then Y in [:X,X:] by A1, TARSKI:def 3;
then consider x, y being set such that
A6: Y = [x,y] by Lm20;
A7: {x} in Y by A6, TARSKI:def 2;
Y c= union X by A5, Lm15;
then {x} in union X by A7, TARSKI:def 3;
then {x} in X \/ (union X) by XBOOLE_0:def 3;
hence contradiction by A4, A7; :: thesis: verum

end;

then Y in union X by A3, XBOOLE_0:def 3;
then consider Z being set such that
A8: Y in Z and
A9: Z in X by TARSKI:def 4;
Z in [:X,X:] by A1, A9, TARSKI:def 3;
then consider x, y being set such that
A10: ( x in X & y in X ) and
A11: Z = [x,y] by Def2;
( Y = {x} or Y = {x,y} ) by A8, A11, TARSKI:def 2;
then ( x in Y & x in X \/ (union X) ) by A10, TARSKI:def 1, TARSKI:def 2, XBOOLE_0:def 3;
hence contradiction by A4; :: thesis: verum