theorem lemBas01: :: REALALG3:20

for F being Field
for E being FieldExtension of F
for a being b₁ -algebraic Element of E holds
( not a in F iff for p being non zero Polynomial of F st Ext_eval (p,a) = 0. E holds
deg p >= 2 )