let X, Y be set ; :: thesis: for W being Relation st X <> {} & Y <> {} & W = [:X,Y:] holds
field W = X \/ Y
let W be Relation; :: thesis: ( X <> {} & Y <> {} & W = [:X,Y:] implies field W = X \/ Y )
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: field W = X \/ Y
A4: for x being object st x in field W holds
x in X \/ Y

proof

let x be object ; :: thesis: ( x in field W implies x in X \/ Y )
assume x in field W ; :: thesis: x in X \/ Y
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: x in X \/ Y
then x in Y by A3, ZFMISC_1:87;
hence x in X \/ Y by XBOOLE_0:def 3; :: thesis: verum

end;

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

proof

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

end;

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

end;

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

proof

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

proof

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

end;

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

proof

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

end;

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

end;

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