set M = { p where p is Polynomial of R : p . (min* { i where i is Nat : p . i <> 0. R } ) in P } ;
now :: thesis: for x being object st x in { p where p is Polynomial of R : p . (min* { i where i is Nat : p . i <> 0. R } ) in P } holds
x in the carrier of (Polynom-Ring R)
let x be object ; :: thesis: ( x in { p where p is Polynomial of R : p . (min* { i where i is Nat : p . i <> 0. R } ) in P } implies x in the carrier of (Polynom-Ring R) )
assume x in { p where p is Polynomial of R : p . (min* { i where i is Nat : p . i <> 0. R } ) in P } ; :: thesis: x in the carrier of (Polynom-Ring R)
then consider p being Polynomial of R such that
H: ( x = p & p . (min* { i where i is Nat : p . i <> 0. R } ) in P ) ;
thus x in the carrier of (Polynom-Ring R) by H, POLYNOM3:def 10; :: thesis: verum
end;
hence { p where p is Polynomial of R : p . (min* { i where i is Nat : p . i <> 0. R } ) in P } is Subset of (Polynom-Ring R) by TARSKI:def 3; :: thesis: verum