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 object such that
A2: z in X by XBOOLE_0:7;
consider Y being set such that
A3: Y in X \/ (union X) and
A4: X \/ (union X) misses Y by A2, XREGULAR:1;

now :: thesis: not Y in X

assume A5: Y in X ; :: thesis: contradiction
then consider x, y being object such that
A6: Y = [x,y] by Lm19, A1;
A7: {x} in Y by A6, TARSKI:def 2;
Y c= union X by A5, Lm14;
then {x} in union X by A7;
then {x} in X \/ (union X) by XBOOLE_0:def 3;
hence contradiction by A4, A7, XBOOLE_0:3; :: 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;
then consider x, y being object such that
A10: x in X and
y in X and
A11: Z = [x,y] by Def2;
( Y = {x} or Y = {x,y} ) by A8, A11, TARSKI:def 2;
then A12: x in Y by TARSKI:def 1, TARSKI:def 2;
x in X \/ (union X) by A10, XBOOLE_0:def 3;
hence contradiction by A4, A12, XBOOLE_0:3; :: thesis: verum