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 set such that
A3: ( x in A & x in B ) by A1, XBOOLE_0:3;
consider y being set such that
A4: ( y in C & y in D ) by A2, XBOOLE_0:3;
A5: [x,y] in [:A,C:] by A3, A4, ZFMISC_1:106;
[x,y] in [:B,D:] by A3, A4, ZFMISC_1:106;
hence [:A,C:] meets [:B,D:] by A5, XBOOLE_0:3; :: thesis: verum