for x being Element of E st x in {a} holds
x is F -algebraic by TARSKI:def 1;
hence for b₁ being Subset of E st b₁ = {a} holds
b₁ is F -algebraic by FIELD_7:def 12; :: thesis: verum