theorem alg1: :: FIELD_7:33
for F being Field
for E being FieldExtension of F
for a being Element of E holds
( a is F -algebraic iff ex B being b1 -finite FieldExtension of F st
( E is B -extending & a in B ) )