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 :: thesis: not X c= [:Y,X:]

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();
consider Y2 being set such that
A5: Y2 in X \/ Z and
A6: X \/ Z misses Y2 by XREGULAR:1, A2;

now :: thesis: ex Y2 being set st
( Y2 in X & ( for Y1 being set st Y1 in Y2 holds
for z being set holds
( not z in Y1 or not z in X ) ) )

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 :: thesis: not Y2 in X

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, XBOOLE_0:3; :: 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, XBOOLE_0:3; :: 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 :: thesis: for y, x being set holds
( not x in X or not Y1 = [y,x] )

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 :: thesis: not X c= [:X,Y:]

consider z being set such that
A19: z in X by A2, XBOOLE_0:7;
consider Y1 being set such that
A20: Y1 in X \/ (union X) and
A21: X \/ (union X) misses Y1 by XREGULAR:1, A19;
assume A22: X c= [:X,Y:] ; :: thesis: contradiction

now :: thesis: not Y1 in X

assume A23: Y1 in X ; :: thesis: contradiction
then consider x, y being set such that
A24: Y1 = [x,y] by Lm20, A22, TARSKI:def 3;
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, XBOOLE_0:3; :: 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, XBOOLE_0:3; :: thesis: verum

end;

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