let x1, x2, x3, y1, y2, y3 be set ; [:{x1,x2,x3},{y1,y2,y3}:] = {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x2,y2],[x2,y3],[x3,y1],[x3,y2],[x3,y3]}
thus [:{x1,x2,x3},{y1,y2,y3}:] =
[:({x1} \/ {x2,x3}),{y1,y2,y3}:]
by ENUMSET1:42
.=
[:({x1} \/ {x2,x3}),({y1} \/ {y2,y3}):]
by ENUMSET1:42
.=
(([:{x1},{y1}:] \/ [:{x1},{y2,y3}:]) \/ [:{x2,x3},{y1}:]) \/ [:{x2,x3},{y2,y3}:]
by ZFMISC_1:121
.=
(([:{x1},{y1}:] \/ [:{x1},{y2,y3}:]) \/ [:{x2,x3},{y1}:]) \/ ([:{x2},{y2,y3}:] \/ [:{x3},{y2,y3}:])
by ZFMISC_1:132
.=
(({[x1,y1]} \/ [:{x1},{y2,y3}:]) \/ [:{x2,x3},{y1}:]) \/ ([:{x2},{y2,y3}:] \/ [:{x3},{y2,y3}:])
by ZFMISC_1:35
.=
(({[x1,y1]} \/ {[x1,y2],[x1,y3]}) \/ [:{x2,x3},{y1}:]) \/ ([:{x2},{y2,y3}:] \/ [:{x3},{y2,y3}:])
by ZFMISC_1:36
.=
(({[x1,y1]} \/ {[x1,y2],[x1,y3]}) \/ {[x2,y1],[x3,y1]}) \/ ([:{x2},{y2,y3}:] \/ [:{x3},{y2,y3}:])
by ZFMISC_1:36
.=
(({[x1,y1]} \/ {[x1,y2],[x1,y3]}) \/ {[x2,y1],[x3,y1]}) \/ ({[x2,y2],[x2,y3]} \/ [:{x3},{y2,y3}:])
by ZFMISC_1:36
.=
(({[x1,y1]} \/ {[x1,y2],[x1,y3]}) \/ {[x2,y1],[x3,y1]}) \/ ({[x2,y2],[x2,y3]} \/ {[x3,y2],[x3,y3]})
by ZFMISC_1:36
.=
({[x1,y1],[x1,y2],[x1,y3]} \/ {[x2,y1],[x3,y1]}) \/ ({[x2,y2],[x2,y3]} \/ {[x3,y2],[x3,y3]})
by ENUMSET1:42
.=
{[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x3,y1]} \/ ({[x2,y2],[x2,y3]} \/ {[x3,y2],[x3,y3]})
by ENUMSET1:49
.=
{[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x3,y1]} \/ {[x2,y2],[x2,y3],[x3,y2],[x3,y3]}
by ENUMSET1:45
.=
{[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x3,y1],[x2,y2],[x2,y3],[x3,y2],[x3,y3]}
by ENUMSET1:131
.=
{[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/ {[x3,y1],[x2,y2],[x2,y3],[x3,y2],[x3,y3]}
by ENUMSET1:130
.=
{[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/ ({[x3,y1],[x2,y2],[x2,y3]} \/ {[x3,y2],[x3,y3]})
by ENUMSET1:49
.=
{[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/ ({[x2,y2],[x2,y3],[x3,y1]} \/ {[x3,y2],[x3,y3]})
by ENUMSET1:100
.=
{[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/ {[x2,y2],[x2,y3],[x3,y1],[x3,y2],[x3,y3]}
by ENUMSET1:49
.=
{[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x2,y2],[x2,y3],[x3,y1],[x3,y2],[x3,y3]}
by ENUMSET1:130
; verum