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

assume X^3-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^3-2 = a * q by FIELD_4:def 5;
thus contradiction by A, thirred, LL; :: thesis: verum

end;

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