now :: thesis: for x being Element of E st x in {a,b} holds
x is F -algebraic

let x be Element of E; :: thesis: ( x in {a,b} implies b₁ is F -algebraic )
assume x in {a,b} ; :: thesis: b₁ is F -algebraic

per cases then ( x = a or x = b ) by TARSKI:def 2;

suppose x = a ; :: thesis: b₁ is F -algebraic

hence x is F -algebraic ; :: thesis: verum

end;

suppose x = b ; :: thesis: b₁ is F -algebraic

hence x is F -algebraic ; :: thesis: verum

end;

end;

end;

hence {a,b} is F -algebraic Subset of E by FIELD_7:def 12; :: thesis: verum