consider A being AlgebraicClosure of F such that
B: E is Subfield of A by XX;
take A ; :: thesis: A is E -extending
thus A is E -extending by B, FIELD_4:7; :: thesis: verum