consider E being FieldExtension of F such that
A: FAdj (F,(Roots (E,p))) is SplittingField of p by spl0;
thus ex b₁ being SplittingField of p st b₁ is strict by A; :: thesis: verum