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