let UN be Universe; :: thesis: ( the carrier of Z_3 in UN & the addF of Z_3 in UN & comp Z_3 in UN & 0. Z_3 in UN & the multF of Z_3 in UN & 1. Z_3 in UN )
thus the carrier of Z_3 in UN by Lm8; :: thesis: ( the addF of Z_3 in UN & comp Z_3 in UN & 0. Z_3 in UN & the multF of Z_3 in UN & 1. Z_3 in UN )
hence ( the addF of Z_3 in UN & comp Z_3 in UN & 0. Z_3 in UN & the multF of Z_3 in UN & 1. Z_3 in UN ) by Lm9, ORDINAL1:10; :: thesis: verum