reconsider K1 = K as FieldExtension of F ;
take K1 ; :: thesis: ( K1 is K -extending & K1 is E -extending )
thus ( K1 is K -extending & K1 is E -extending ) by FIELD_4:6; :: thesis: verum