let x1, x2, y1, y2 be set ; :: thesis: [:{x1,x2},{y1,y2}:] = {[x1,y1],[x1,y2],[x2,y1],[x2,y2]}
thus [:{x1,x2},{y1,y2}:] = [:({x1} \/ {x2}),{y1,y2}:] by ENUMSET1:1
.= [:{x1},{y1,y2}:] \/ [:{x2},{y1,y2}:] by Th120
.= {[x1,y1],[x1,y2]} \/ [:{x2},{y1,y2}:] by Th36
.= {[x1,y1],[x1,y2]} \/ {[x2,y1],[x2,y2]} by Th36
.= {[x1,y1],[x1,y2],[x2,y1],[x2,y2]} by ENUMSET1:5 ; :: thesis: verum