let X, Y be set ; :: thesis: ( ( X c= [:X,Y:] or X c= [:Y,X:] ) implies X = {} )
assume A1: ( X c= [:X,Y:] or X c= [:Y,X:] ) ; :: thesis: X = {}
assume A2: X <> {} ; :: thesis: contradiction

A3: now

defpred S₁[ set ] means ex Y being set st
( $1 = Y & ex z being set st
( z in Y & z in X ) );
consider Z being set such that
A4: for y being set holds
( y in Z iff ( y in union X & S₁[y] ) ) from XBOOLE_0:sch 1();
ex x being set st x in X \/ Z by A2, XBOOLE_0:7;
then consider Y2 being set such that
A5: Y2 in X \/ Z and
A6: for x being set holds
( not x in X \/ Z or not x in Y2 ) by TARSKI:2;

now

assume A7: for Y2 being set holds
( not Y2 in X or ex Y1 being set st
( Y1 in Y2 & ex z being set st
( z in Y1 & z in X ) ) ) ; :: thesis: contradiction

now

assume A8: Y2 in X ; :: thesis: contradiction
then consider Y1 being set such that
A9: Y1 in Y2 and
A10: ex z being set st
( z in Y1 & z in X ) by A7;
Y1 in union X by A8, A9, TARSKI:def 4;
then Y1 in Z by A4, A10;
then Y1 in X \/ Z by XBOOLE_0:def 3;
hence contradiction by A6, A9; :: thesis: verum

end;

then Y2 in Z by A5, XBOOLE_0:def 3;
then ex X2 being set st
( Y2 = X2 & ex z being set st
( z in X2 & z in X ) ) by A4;
then consider z being set such that
A11: z in Y2 and
A12: z in X ;
z in X \/ Z by A12, XBOOLE_0:def 3;
hence contradiction by A6, A11; :: thesis: verum

end;

then consider Y1 being set such that
A13: Y1 in X and
A14: for Y2 being set holds
( not Y2 in Y1 or for z being set holds
( not z in Y2 or not z in X ) ) ;

A15: now

given y, x being set such that A16: x in X and
A17: Y1 = [y,x] ; :: thesis: contradiction
A18: x in {y,x} by TARSKI:def 2;
{y,x} in Y1 by A17, TARSKI:def 2;
hence contradiction by A14, A16, A18; :: thesis: verum

end;

assume X c= [:Y,X:] ; :: thesis: contradiction
then Y1 in [:Y,X:] by A13, TARSKI:def 3;
then ex y, x being set st
( y in Y & x in X & Y1 = [y,x] ) by Def2;
hence contradiction by A15; :: thesis: verum

end;

now

consider z being set such that
A19: z in X by A2, XBOOLE_0:7;
z in X \/ (union X) by A19, XBOOLE_0:def 3;
then consider Y1 being set such that
A20: Y1 in X \/ (union X) and
A21: for x being set holds
( not x in X \/ (union X) or not x in Y1 ) by TARSKI:2;
assume A22: X c= [:X,Y:] ; :: thesis: contradiction

now

assume A23: Y1 in X ; :: thesis: contradiction
then Y1 in [:X,Y:] by A22, TARSKI:def 3;
then consider x, y being set such that
A24: Y1 = [x,y] by Lm20;
A25: {x} in Y1 by A24, TARSKI:def 2;
Y1 c= union X by A23, Lm15;
then {x} in union X by A25, TARSKI:def 3;
then {x} in X \/ (union X) by XBOOLE_0:def 3;
hence contradiction by A21, A25; :: thesis: verum

end;

then Y1 in union X by A20, XBOOLE_0:def 3;
then consider Y2 being set such that
A26: Y1 in Y2 and
A27: Y2 in X by TARSKI:def 4;
Y2 in [:X,Y:] by A22, A27, TARSKI:def 3;
then consider x, y being set such that
A28: x in X and
y in Y and
A29: Y2 = [x,y] by Def2;
( Y1 = {x} or Y1 = {x,y} ) by A26, A29, TARSKI:def 2;
then A30: x in Y1 by TARSKI:def 1, TARSKI:def 2;
x in X \/ (union X) by A28, XBOOLE_0:def 3;
hence contradiction by A21, A30; :: thesis: verum

end;

hence contradiction by A1, A3; :: thesis: verum