now :: thesis: for x being Element of E st x in T1 \ T2 holds
x is F -algebraic

let x be Element of E; :: thesis: ( x in T1 \ T2 implies x is F -algebraic )
assume x in T1 \ T2 ; :: thesis: x is F -algebraic
then x in T1 by XBOOLE_0:def 5;
hence x is F -algebraic by FIELD_7:def 12; :: thesis: verum

end;

hence for b₁ being Subset of E st b₁ = T1 \ T2 holds
b₁ is F -algebraic by FIELD_7:def 12; :: thesis: verum