set p = X^3-1 ;
set F = F_Rat ;
LC X^3-1 = X^3-1 . (4 -' 1) by LL1, RATFUNC1:def 6
.= X^3-1 . (4 - 1) by XREAL_0:def 2
.= 1. F_Rat by LL01, GAUSSINT:def 14 ;
hence X^3-1 is monic by RATFUNC1:def 7; :: thesis: ( not X^3-1 is constant & not X^3-1 is irreducible )
thus not X^3-1 is constant by LL, RING_4:def 4; :: thesis: not X^3-1 is irreducible
eval (X^3-1,(1. F_Rat)) = ((1. F_Rat) |^ 3) - 1 by LL31
.= (1 |^ 3) - 1 by lem3, GAUSSINT:def 14
.= 0. F_Rat by GAUSSINT:def 14 ;
then X^3-1 is with_roots by POLYNOM5:def 7, POLYNOM5:def 8;
hence X^3-1 is reducible by LL, thirred; :: thesis: verum