ex b being F -algebraic Element of E st
( b = a & MinPoly (b,F) is separable ) by defsep;
hence MinPoly (a,F) is separable ; :: thesis: verum