consider E being FieldExtension of F such that
A:
p splits_in E
by FIELD_5:31;
take K = FAdj (F,(Roots (E,p))); ( p splits_in K & ( for E being FieldExtension of F st p splits_in E & E is Subfield of K holds
E == K ) )
thus
p splits_in K
by A, lemma5; for E being FieldExtension of F st p splits_in E & E is Subfield of K holds
E == K
now for U being FieldExtension of F st p splits_in U & U is Subfield of K holds
U == Klet U be
FieldExtension of
F;
( p splits_in U & U is Subfield of K implies U == K )assume B:
(
p splits_in U &
U is
Subfield of
K )
;
U == KC:
U is
Subfield of
E
by B, EC_PF_1:5;
then C1:
E is
FieldExtension of
U
by FIELD_4:7;
D:
F is
Subfield of
U
by FIELD_4:7;
E:
Roots (
U,
p)
c= Roots (
E,
p)
by C1, lemma7;
Roots (
E,
p)
c= Roots (
U,
p)
by C1, A, B, lemma3;
then
Roots (
E,
p) is
Subset of
U
by E, XBOOLE_0:def 10;
hence
U == K
by B, D, C, FIELD_6:37;
verum end;
hence
for E being FieldExtension of F st p splits_in E & E is Subfield of K holds
E == K
; verum