:: deftheorem defsepF defines -separable FIELD_15:def 6 :
for F being Field
for E being FieldExtension of F holds
( E is F -separable iff ( E is F -algebraic & ( for a being Element of E holds a is F -separable ) ) );