let X1, X2, Y1, Y2 be set ; :: thesis: ( ( X1 misses X2 or Y1 misses Y2 ) implies [:X1,Y1:] misses [:X2,Y2:] )
assume A1: ( X1 misses X2 or Y1 misses Y2 ) ; :: thesis: [:X1,Y1:] misses [:X2,Y2:]
assume not [:X1,Y1:] misses [:X2,Y2:] ; :: thesis: contradiction
then consider z being set such that
A2: z in [:X1,Y1:] /\ [:X2,Y2:] by XBOOLE_0:4;
ex x, y being set st
( z = [x,y] & x in X1 /\ X2 & y in Y1 /\ Y2 ) by A2, Th104;
hence contradiction by A1, XBOOLE_0:4; :: thesis: verum