theorem simp2: :: FIELD_14:5

for F being Field
for E being FieldExtension of F
for K being b₁ -extending FieldExtension of F holds IntermediateFields (E,F) c= IntermediateFields (K,F)