deg (X+ a) = 1 by HURWITZ:27;
hence X+ a is linear by FIELD_5:def 1; :: thesis: X+ a is monic
thus X+ a is monic ; :: thesis: verum