A: now :: thesis: for o being object st o in { p where p is non constant Element of the carrier of (Polynom-Ring F) : verum } holds
o in the carrier of (Polynom-Ring F)

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

end;

set p = the non constant Element of the carrier of (Polynom-Ring F);
the non constant Element of the carrier of (Polynom-Ring F) in { p where p is non constant Element of the carrier of (Polynom-Ring F) : verum } ;
hence { p where p is non constant Element of the carrier of (Polynom-Ring F) : verum } is non empty Subset of the carrier of (Polynom-Ring F) by A, TARSKI:def 3; :: thesis: verum