take K ; :: thesis: K is K -extending
thus K is K -extending by FIELD_4:6; :: thesis: verum