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 b₁ is F -algebraic )
assume x in T1 \/ T2 ; :: thesis: b₁ is F -algebraic

per cases then ( x in T1 or x in T2 ) by XBOOLE_0:def 3;

suppose x in T1 ; :: thesis: b₁ is F -algebraic

hence x is F -algebraic by FIELD_7:def 12; :: thesis: verum

end;

suppose x in T2 ; :: thesis: b₁ is F -algebraic

hence x is F -algebraic by FIELD_7:def 12; :: thesis: verum

end;

end;

end;

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