now :: thesis: for a being Element of E st a in Roots (E,p) holds
a is F -algebraic

let a be Element of E; :: thesis: ( a in Roots (E,p) implies a is F -algebraic )
assume a in Roots (E,p) ; :: thesis: a is F -algebraic
then a in { a where a is Element of E : a is_a_root_of p,E } by FIELD_4:def 4;
then consider b being Element of E such that
A: ( b = a & b is_a_root_of p,E ) ;
Ext_eval (p,a) = 0. E by A, FIELD_4:def 2;
hence a is F -algebraic by FIELD_6:43; :: thesis: verum

end;

hence Roots (E,p) is F -algebraic ; :: thesis: verum