let X, Y be set ; :: thesis:
let W be Relation; :: thesis:
set a = the Element of X;
set b = the Element of Y;
assume that
A1: X <> {} and
A2: Y <> {} and
A3: W = [:X,Y:] ; :: thesis:
A4: for x being object st x in field W holds
x in X \/ Y

proof

let x be object ; :: thesis:
assume x in field W ; :: thesis:
then consider y being object such that
A5: ( [x,y] in W or [y,x] in W ) by Th1;
A6: ( [y,x] in W implies x in X \/ Y )

proof

assume [y,x] in W ; :: thesis:
then x in Y by A3, ZFMISC_1:87;
hence x in X \/ Y by XBOOLE_0:def 3; :: thesis:

end;

( [x,y] in W implies x in X \/ Y )

proof

assume [x,y] in W ; :: thesis:
then x in X by A3, ZFMISC_1:87;
hence x in X \/ Y by XBOOLE_0:def 3; :: thesis:

end;

hence x in X \/ Y by A5, A6; :: thesis:

end;

for x being object st x in X \/ Y holds
x in field W

proof

let x be object ; :: thesis:
A7: ( x in X implies x in field W )

proof

assume x in X ; :: thesis:
then [x, the Element of Y] in W by A2, A3, ZFMISC_1:87;
hence x in field W by Th1; :: thesis:

end;

A8: ( x in Y implies x in field W )

proof

assume x in Y ; :: thesis:
then [ the Element of X,x] in W by A1, A3, ZFMISC_1:87;
hence x in field W by Th1; :: thesis:

end;

assume x in X \/ Y ; :: thesis:
hence x in field W by A7, A8, XBOOLE_0:def 3; :: thesis:

end;

hence field W = X \/ Y by A4, TARSKI:2; :: thesis: