not sqrt 2 in RAT by INT_2:28, IRRAT_1:1;
hence not 2-Root(2) is F_Rat -membered by GAUSSINT:def 14, FIELD_7:def 5; :: thesis: 2-Root(2) is F_Rat -algebraic
Ext_eval (X^2-2,2-Root(2)) = (2-Root(2) |^ (1 + 1)) - 2 by LKX2ext
.= ((2-Root(2) |^ 1) * (2-Root(2) |^ 1)) - 2 by BINOM:10
.= (2-Root(2) * (2-Root(2) |^ 1)) - 2 by BINOM:8
.= (2-Root(2) * 2-Root(2)) - 2 by BINOM:8
.= ((sqrt 2) ^2) - 2 by SQUARE_1:def 1
.= 2 - 2 by SQUARE_1:def 2
.= 0. F_Real ;
hence 2-Root(2) is F_Rat -algebraic by FIELD_6:43; :: thesis: verum