let
X
,
Y
be
set
;
:: thesis:
union
{
X
,
Y
,
{}
}
=
union
{
X
,
Y
}
thus
union
{
X
,
Y
,
{}
}
=
union
(
{
X
,
Y
}
\/
{
{}
}
)
by
ENUMSET1:3
.=
(
union
{
X
,
Y
}
)
\/
(
union
{
{}
}
)
by
ZFMISC_1:78
.=
(
union
{
X
,
Y
}
)
\/
{}
by
ZFMISC_1:25
.=
union
{
X
,
Y
}
;
:: thesis:
verum