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