let
UN
be
Universe
;
:: thesis:
the
carrier
of
Z_3
in
UN
reconsider
a
=
0
,
b
= 1,
c
= 2 as
Element
of
UN
by
Th21
;
{
a
,
b
,
c
}
is
Element
of
UN
by
Th19
;
hence
the
carrier
of
Z_3
in
UN
;
:: thesis:
verum