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

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

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

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

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

end;

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

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

end;

end;

end;

then {a,b} is F -algebraic ;
hence FAdj (F,{a,b}) is F -finite ; :: thesis: verum