set F = F_Real ;
set p = X^2-2 ;
set M = {2-Root(2),(- 2-Root(2))};
H: Roots (F_Real,X^2-2) = { a where a is Element of F_Real : a is_a_root_of X^2-2 , F_Real } by FIELD_4:def 4;

now :: thesis: for o being object st o in {2-Root(2),(- 2-Root(2))} holds
o in Roots (F_Real,X^2-2)

let o be object ; :: thesis: ( o in {2-Root(2),(- 2-Root(2))} implies b₁ in Roots (F_Real,X^2-2) )
assume B: o in {2-Root(2),(- 2-Root(2))} ; :: thesis: b₁ in Roots (F_Real,X^2-2)
then reconsider c = o as Element of F_Real ;

per cases ( o = 2-Root(2) or o = - 2-Root(2) ) by B, TARSKI:def 2;

suppose E0: o = 2-Root(2) ; :: thesis: b₁ in Roots (F_Real,X^2-2)

Ext_eval (X^2-2,c) = (2-Root(2) |^ (1 + 1)) - 2 by E0, LKX2ext
.= ((2-Root(2) |^ 1) * (2-Root(2) |^ 1)) - 2 by BINOM:10
.= ((2-Root(2) |^ 1) * 2-Root(2)) - 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 ;
then c is_a_root_of X^2-2 , F_Real by FIELD_4:def 2;
hence o in Roots (F_Real,X^2-2) by H; :: thesis: verum

end;

suppose E0: o = - 2-Root(2) ; :: thesis: b₁ in Roots (F_Real,X^2-2)

Ext_eval (X^2-2,c) = ((- 2-Root(2)) |^ (1 + 1)) - 2 by E0, LKX2ext
.= (((- 2-Root(2)) |^ 1) * ((- 2-Root(2)) |^ 1)) - 2 by BINOM:10
.= (((- 2-Root(2)) |^ 1) * (- 2-Root(2))) - 2 by BINOM:8
.= ((- 2-Root(2)) * (- 2-Root(2))) - 2 by BINOM:8
.= (2-Root(2) * 2-Root(2)) - 2
.= ((sqrt 2) ^2) - 2 by SQUARE_1:def 1
.= 2 - 2 by SQUARE_1:def 2
.= 0. F_Real ;
then c is_a_root_of X^2-2 , F_Real by FIELD_4:def 2;
hence o in Roots (F_Real,X^2-2) by H; :: thesis: verum

end;

end;

end;

then B: {2-Root(2),(- 2-Root(2))} c= Roots (F_Real,X^2-2) ;
the carrier of (Polynom-Ring F_Rat) c= the carrier of (Polynom-Ring F_Real) by FIELD_4:10;
then reconsider q = X^2-2 as Element of the carrier of (Polynom-Ring F_Real) ;
reconsider qq = q as non zero Element of the carrier of (Polynom-Ring F_Rat) ;
H: 2 = deg X^2-2 by FIELD_9:18
.= deg q by FIELD_4:20 ;
then reconsider q = q as non constant Element of the carrier of (Polynom-Ring F_Real) by RING_4:def 4;
C: card {2-Root(2),(- 2-Root(2))} = 2 by CARD_2:57, SQUARE_1:19;
D: card (Roots (F_Real,X^2-2)) = 2

proof

F: card (Roots q) <= 2 by H, RING_5:22;
G: 2 <= card (Roots (F_Real,qq)) by C, B, NAT_1:43;
Roots (F_Real,X^2-2) = Roots q by FIELD_7:13;
hence card (Roots (F_Real,X^2-2)) = 2 by F, G, XXREAL_0:1; :: thesis: verum

end;

thus Roots (F_Real,X^2-2) = {2-Root(2),(- 2-Root(2))} by B, C, D, lemfinset; :: thesis: verum