let
x
,
y
,
z
be
set
;
:: thesis:
rng
<*
x
,
y
,
z
*>
=
{
x
,
y
,
z
}
thus
rng
<*
x
,
y
,
z
*>
=
(
rng
<*
x
,
y
*>
)
\/
(
rng
<*
z
*>
)
by
FINSEQ_1:31
.=
{
x
,
y
}
\/
(
rng
<*
z
*>
)
by
Lm1
.=
{
x
,
y
}
\/
{
z
}
by
FINSEQ_1:38
.=
{
x
,
y
,
z
}
by
ENUMSET1:3
;
:: thesis:
verum