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:2
.=
[:({x1} \/ {x2,x3}),({y1} \/ {y2,y3}):]
by ENUMSET1:2
.=
(([:{x1},{y1}:] \/ [:{x1},{y2,y3}:]) \/ [:{x2,x3},{y1}:]) \/ [:{x2,x3},{y2,y3}:]
by ZFMISC_1:98
.=
(([:{x1},{y1}:] \/ [:{x1},{y2,y3}:]) \/ [:{x2,x3},{y1}:]) \/ ([:{x2},{y2,y3}:] \/ [:{x3},{y2,y3}:])
by ZFMISC_1:109
.=
(({[x1,y1]} \/ [:{x1},{y2,y3}:]) \/ [:{x2,x3},{y1}:]) \/ ([:{x2},{y2,y3}:] \/ [:{x3},{y2,y3}:])
by ZFMISC_1:29
.=
(({[x1,y1]} \/ {[x1,y2],[x1,y3]}) \/ [:{x2,x3},{y1}:]) \/ ([:{x2},{y2,y3}:] \/ [:{x3},{y2,y3}:])
by ZFMISC_1:30
.=
(({[x1,y1]} \/ {[x1,y2],[x1,y3]}) \/ {[x2,y1],[x3,y1]}) \/ ([:{x2},{y2,y3}:] \/ [:{x3},{y2,y3}:])
by ZFMISC_1:30
.=
(({[x1,y1]} \/ {[x1,y2],[x1,y3]}) \/ {[x2,y1],[x3,y1]}) \/ ({[x2,y2],[x2,y3]} \/ [:{x3},{y2,y3}:])
by ZFMISC_1:30
.=
(({[x1,y1]} \/ {[x1,y2],[x1,y3]}) \/ {[x2,y1],[x3,y1]}) \/ ({[x2,y2],[x2,y3]} \/ {[x3,y2],[x3,y3]})
by ZFMISC_1:30
.=
({[x1,y1],[x1,y2],[x1,y3]} \/ {[x2,y1],[x3,y1]}) \/ ({[x2,y2],[x2,y3]} \/ {[x3,y2],[x3,y3]})
by ENUMSET1:2
.=
{[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x3,y1]} \/ ({[x2,y2],[x2,y3]} \/ {[x3,y2],[x3,y3]})
by ENUMSET1:9
.=
{[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x3,y1]} \/ {[x2,y2],[x2,y3],[x3,y2],[x3,y3]}
by ENUMSET1:5
.=
{[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x3,y1],[x2,y2],[x2,y3],[x3,y2],[x3,y3]}
by ENUMSET1:81
.=
{[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/ {[x3,y1],[x2,y2],[x2,y3],[x3,y2],[x3,y3]}
by ENUMSET1:80
.=
{[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/ ({[x3,y1],[x2,y2],[x2,y3]} \/ {[x3,y2],[x3,y3]})
by ENUMSET1:9
.=
{[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/ ({[x2,y2],[x2,y3],[x3,y1]} \/ {[x3,y2],[x3,y3]})
by ENUMSET1:59
.=
{[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/ {[x2,y2],[x2,y3],[x3,y1],[x3,y2],[x3,y3]}
by ENUMSET1:9
.=
{[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x2,y2],[x2,y3],[x3,y1],[x3,y2],[x3,y3]}
by ENUMSET1:80
; verum