now :: thesis: not X^2-2 splits_in F_Rat

assume X^2-2 splits_in F_Rat ; :: thesis: contradiction
then consider a being non zero Element of F_Rat, q being Ppoly of F_Rat such that
A: X^2-2 = a * q by FIELD_4:def 5;
thus contradiction by A; :: thesis: verum

end;

hence not X^2-2 splits_in F_Rat ; :: thesis: verum