let x be Element of F_Real; :: thesis: ( x is irrational implies for g being non zero Polynomial of F_Rat st Ext_eval (g,x) = 0 holds
deg g >= 2 )
assume A1: x is irrational ; :: thesis: for g being non zero Polynomial of F_Rat st Ext_eval (g,x) = 0 holds
deg g >= 2
let g be non zero Polynomial of F_Rat; :: thesis: ( Ext_eval (g,x) = 0 implies deg g >= 2 )
assume A2: Ext_eval (g,x) = 0 ; :: thesis: deg g >= 2
assume not deg g >= 2 ; :: thesis: contradiction
then consider y, z being Element of F_Rat such that
A4: g = <%y,z%> by FIELD_9:13;
A5: 0 = (In (y,F_Real)) + ((In (z,F_Real)) * x) by ALGNUM_1:22, LIOUVIL2:4, A4, A2;

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

suppose z = 0 ; :: thesis: contradiction

then g = 0_. F_Rat by A5, GAUSSINT:def 14, A4, POLYNOM5:42;
hence contradiction ; :: thesis: verum

end;

suppose z <> 0 ; :: thesis: contradiction

hence contradiction by A1, A5; :: thesis: verum

end;

end;