A: FAdj (F,{a,b}) is Subring of E by FIELD_5:12;
then reconsider E1 = E as F -extending FieldExtension of F by FIELD_4:def 1;
B: {a,b} is Subset of (FAdj (F,{a,b})) by FIELD_6:35;
a in {a,b} by TARSKI:def 2;
then reconsider a1 = a as Element of the carrier of (FAdj (F,{a,b})) by B;
b in {a,b} by TARSKI:def 2;
then reconsider b1 = b as Element of the carrier of (FAdj (F,{a,b})) by B;
- b = - b1 by A, FIELD_6:17;
then a + (- b) = a1 + (- b1) by A, FIELD_6:15;
then reconsider c = a - b as FAdj (F,{a,b}) -membered Element of E1 by defmem;
@ ((@ ((FAdj (F,{a,b})),c)),E1) is F -algebraic ;
hence a - b is F -algebraic ; :: thesis: verum