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