take E ; :: thesis: E is E -extending
E is Subring of E by LIOUVIL2:18;
hence E is E -extending by FIELD_4:def 1; :: thesis: verum