theorem :: MCART_1:85

for x1, x2, y, y1, y2, x being object holds
( [[x1,x2],y] `11 = x1 & [[x1,x2],y] `12 = x2 & [x,[y1,y2]] `21 = y1 & [x,[y1,y2]] `22 = y2 ) ;