let z be object ; :: thesis: for X1, X2, Y1, Y2 being set st z in [:X1,Y1:] /\ [:X2,Y2:] holds
ex x, y being object st
( z = [x,y] & x in X1 /\ X2 & y in Y1 /\ Y2 )
let X1, X2, Y1, Y2 be set ; :: thesis: ( z in [:X1,Y1:] /\ [:X2,Y2:] implies ex x, y being object st
( z = [x,y] & x in X1 /\ X2 & y in Y1 /\ Y2 ) )
assume A1: z in [:X1,Y1:] /\ [:X2,Y2:] ; :: thesis: ex x, y being object st
( z = [x,y] & x in X1 /\ X2 & y in Y1 /\ Y2 )
then z in [:X1,Y1:] by XBOOLE_0:def 4;
then consider x1, y1 being object such that
A2: x1 in X1 and
A3: y1 in Y1 and
A4: z = [x1,y1] by Def2;
z in [:X2,Y2:] by A1, XBOOLE_0:def 4;
then consider x2, y2 being object such that
A5: x2 in X2 and
A6: y2 in Y2 and
A7: z = [x2,y2] by Def2;
y1 = y2 by A4, A7, XTUPLE_0:1;
then A8: y1 in Y1 /\ Y2 by A3, A6, XBOOLE_0:def 4;
x1 = x2 by A4, A7, XTUPLE_0:1;
then x1 in X1 /\ X2 by A2, A5, XBOOLE_0:def 4;
hence ex x, y being object st
( z = [x,y] & x in X1 /\ X2 & y in Y1 /\ Y2 ) by A4, A8; :: thesis: verum