:: deftheorem defines alpha FIELD_9:def 18 :
alpha = KrRootP X^2+X+1;