let
X1
,
X2
,
X3
be
set
;
:: thesis:
union
{
X1
,
X2
,
X3
}
=
(
X1
\/
X2
)
\/
X3
thus
union
{
X1
,
X2
,
X3
}
=
union
(
{
X1
,
X2
}
\/
{
X3
}
)
by
ENUMSET1:3
.=
(
union
{
X1
,
X2
}
)
\/
(
union
{
X3
}
)
by
ZFMISC_1:78
.=
(
X1
\/
X2
)
\/
(
union
{
X3
}
)
by
ZFMISC_1:75
.=
(
X1
\/
X2
)
\/
X3
;
:: thesis:
verum