theorem lemBas0: :: REALALG3:19

for F being Field
for E being FieldExtension of F
for a being Element of E st a ^2 in F holds
a is F -algebraic