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

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

now

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

end;

then Y1 in union X by A6, XBOOLE_0:def 3;
then consider Y2 being set such that
A11: Y1 in Y2 and
A12: Y2 in X by TARSKI:def 4;
Y2 in [:X,Y:] by A4, A12, TARSKI:def 3;
then consider x, y being set such that
A13: ( x in X & y in Y ) and
A14: Y2 = [x,y] by Def2;
( Y1 = {x} or Y1 = {x,y} ) by A11, A14, TARSKI:def 2;
then ( x in Y1 & x in X \/ (union X) ) by A13, TARSKI:def 1, TARSKI:def 2, XBOOLE_0:def 3;
hence contradiction by A7; :: thesis: verum

end;

now

assume A15: X c= [:Y,X:] ; :: thesis: contradiction
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
A16: for y being set holds
( y in Z iff ( y in union X & S₁[y] ) ) from XBOOLE_0:sch 1();
X \/ Z <> {} by A2;
then consider x being set such that
A17: x in X \/ Z by XBOOLE_0:7;
consider Y2 being set such that
A18: Y2 in X \/ Z and
A19: for x being set holds
( not x in X \/ Z or not x in Y2 ) by A17, TARSKI:7;

now

assume A20: 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 A21: Y2 in X ; :: thesis: contradiction
then consider Y1 being set such that
A22: Y1 in Y2 and
A23: ex z being set st
( z in Y1 & z in X ) by A20;
Y1 in union X by A21, A22, TARSKI:def 4;
then Y1 in Z by A16, A23;
then Y1 in X \/ Z by XBOOLE_0:def 3;
hence contradiction by A19, A22; :: thesis: verum

end;

then Y2 in Z by A18, XBOOLE_0:def 3;
then ex X2 being set st
( Y2 = X2 & ex z being set st
( z in X2 & z in X ) ) by A16;
then consider z being set such that
A24: z in Y2 and
A25: z in X ;
z in X \/ Z by A25, XBOOLE_0:def 3;
hence contradiction by A19, A24; :: thesis: verum

end;

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

A28: now

given y, x being set such that A29: x in X and
A30: Y1 = [y,x] ; :: thesis: contradiction
( {y,x} in Y1 & x in {y,x} ) by A30, TARSKI:def 2;
hence contradiction by A27, A29; :: thesis: verum

end;

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

end;

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