now :: thesis: for o being object st o in { a where a is F -algebraic Element of E : verum } holds
o in the carrier of E

let o be object ; :: thesis: ( o in { a where a is F -algebraic Element of E : verum } implies o in the carrier of E )
assume o in { a where a is F -algebraic Element of E : verum } ; :: thesis: o in the carrier of E
then consider a being F -algebraic Element of E such that
A: a = o ;
thus o in the carrier of E by A; :: thesis: verum

end;

hence { a where a is F -algebraic Element of E : verum } is Subset of E by TARSKI:def 3; :: thesis: verum