theorem lemBas1: :: REALALG3:21

for F being Field
for E being FieldExtension of F
for a being b₁ -algebraic Element of E st not a in F holds
for b being Element of F st b = a ^2 holds
MinPoly (a,F) = X^2- b