set p = X^3-2 ;
set F = F_Rat ;
LC X^3-2 = X^3-2 . (4 -' 1) by LL1, RATFUNC1:def 6
.= X^3-2 . (4 - 1) by XREAL_0:def 2
.= 1. F_Rat by LL0, GAUSSINT:def 14 ;
hence X^3-2 is monic by RATFUNC1:def 7; :: thesis: ( not X^3-2 is constant & X^3-2 is irreducible )
thus not X^3-2 is constant by LL, RING_4:def 4; :: thesis: X^3-2 is irreducible

now :: thesis: not X^3-2 is with_roots

assume X^3-2 is with_roots ; :: thesis: contradiction
then consider a being Element of F_Rat such that
A: a is_a_root_of X^3-2 by POLYNOM5:def 8;
reconsider r = a as Rational ;
0. F_Rat = eval (X^3-2,a) by A, POLYNOM5:def 7
.= (a |^ 3) - 2 by LL3 ;
then 2 = r |^ 3 by lem3, GAUSSINT:def 14;
hence contradiction by lemcontr; :: thesis: verum

end;

hence X^3-2 is irreducible by LL, thirred; :: thesis: verum