now :: thesis: for o being object st o in { x where x is Polynomial of R : LC x in P } holds
o in the carrier of (Polynom-Ring R)

let o be object ; :: thesis: ( o in { x where x is Polynomial of R : LC x in P } implies o in the carrier of (Polynom-Ring R) )
assume o in { x where x is Polynomial of R : LC x in P } ; :: thesis: o in the carrier of (Polynom-Ring R)
then consider x being Polynomial of R such that
A: ( o = x & LC x in P ) ;
thus o in the carrier of (Polynom-Ring R) by A, POLYNOM3:def 10; :: thesis: verum

end;

hence { p where p is Polynomial of R : LC p in P } is Subset of (Polynom-Ring R) by TARSKI:def 3; :: thesis: verum