let A, B, C, D be set ; :: thesis: ( A meets B & C meets D implies [:A,C:] meets [:B,D:] )
assume that
A1: A meets B and
A2: C meets D ; :: thesis: [:A,C:] meets [:B,D:]
consider x being object such that
A3: ( x in A & x in B ) by A1, XBOOLE_0:3;
consider y being object such that
A4: ( y in C & y in D ) by A2, XBOOLE_0:3;
( [x,y] in [:A,C:] & [x,y] in [:B,D:] ) by A3, A4, ZFMISC_1:87;
hence [:A,C:] meets [:B,D:] by XBOOLE_0:3; :: thesis: verum