set M = { q where q is Element of the carrier of (Polynom-Ring R) : q divides p } ;

now :: thesis: for o being object st o in { q where q is Element of the carrier of (Polynom-Ring R) : q divides p } holds
o in the carrier of (Polynom-Ring R)

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

end;

then B: { q where q is Element of the carrier of (Polynom-Ring R) : q divides p } c= the carrier of (Polynom-Ring R) ;
C: 1_. R is Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
(1_. R) *' p = p ;
then 1_. R divides p by RING_4:1;
then 1_. R in { q where q is Element of the carrier of (Polynom-Ring R) : q divides p } by C;
hence { q where q is Element of the carrier of (Polynom-Ring R) : q divides p } is non empty Subset of the carrier of (Polynom-Ring R) by B; :: thesis: verum