let
UN
be
Universe
;
:: thesis:
for
u
,
v
,
w
being
Element
of
UN
holds
{
u
,
v
,
w
}
is
Element
of
UN
let
u
,
v
,
w
be
Element
of
UN
;
:: thesis:
{
u
,
v
,
w
}
is
Element
of
UN
{
u
,
v
,
w
}
=
{
u
,
v
}
\/
{
w
}
by
ENUMSET1:3
;
hence
{
u
,
v
,
w
}
is
Element
of
UN
;
:: thesis:
verum