let X, Y be set ; :: thesis: ( X c= [:X,Y:] implies X = {} )
assume A1: X c= [:X,Y:] ; :: thesis: X = {}
assume X <> {} ; :: thesis: contradiction
then consider z being object such that
A2: z in X by XBOOLE_0:7;
consider M being set such that
A3: M in X \/ (union X) and
A4: X \/ (union X) misses M by A2, XREGULAR:1;
now :: thesis: not M in X
assume A5: M in X ; :: thesis: contradiction
then consider x, y being object such that
A6: M = [x,y] by Lm19, A1;
A7: {x} in M by A6, TARSKI:def 2;
M 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 M in union X by A3, XBOOLE_0:def 3;
then consider Z being set such that
A8: M in Z and
A9: Z in X by TARSKI:def 4;
Z in [:X,Y:] by A1, A9;
then consider x, y being object such that
A10: x in X and
y in Y and
A11: Z = [x,y] by Def2;
( M = {x} or M = {x,y} ) by A8, A11, TARSKI:def 2;
then A12: x in M 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