set p = X^2-2 ;
set F = F_Rat ;
thus X^2-2 is monic ; :: thesis: ( X^2-2 is purely_quadratic & X^2-2 is irreducible )
thus X^2-2 is purely_quadratic ; :: thesis: X^2-2 is irreducible

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

assume X^2-2 is with_roots ; :: thesis: contradiction
then consider a being Element of F_Rat such that
A: a is_a_root_of X^2-2 by POLYNOM5:def 8;
reconsider r = a as Rational ;
0. F_Rat = eval (X^2-2,a) by A, POLYNOM5:def 7
.= (a |^ 2) - 2 by LKX2 ;
then B: 2 = a |^ (1 + 1) by GAUSSINT:def 14
.= (a |^ 1) * (a |^ 1) by BINOM:10
.= a * (a |^ 1) by BINOM:8
.= r * r by BINOM:8
.= r ^2 by SQUARE_1:def 1 ;

per cases ( r >= 0 or r <= 0 ) ;

suppose r >= 0 ; :: thesis: contradiction

then r = sqrt 2 by B, SQUARE_1:def 2;
hence contradiction by INT_2:28, IRRAT_1:1; :: thesis: verum

end;

suppose L: r <= 0 ; :: thesis: contradiction

(- r) ^2 = r ^2 by SQUARE_1:3;
then - r = sqrt 2 by L, B, SQUARE_1:def 2;
hence contradiction by INT_2:28, IRRAT_1:1; :: thesis: verum

end;

end;

end;

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