theorem :: FIELD_10:14

( zeta |^ 2 <> 1 & zeta |^ 3 = 1 & zeta |^ 2 = (- zeta) - 1 ) by LZ23;