theorem :: ZFMISC_1:122

for x1, x2, y1, y2 being object holds [:{x1,x2},{y1,y2}:] = {[x1,y1],[x1,y2],[x2,y1],[x2,y2]}