theorem 2splitb: :: FIELD_10:35

Roots (F_Real,X^2-2) = {2-Root(2),(- 2-Root(2))}