now :: thesis: for u being object st u in {p} holds
u in the carrier of (Polynom-Ring (n,L))

let u be object ; :: thesis: ( u in {p} implies u in the carrier of (Polynom-Ring (n,L)) )
assume u in {p} ; :: thesis: u in the carrier of (Polynom-Ring (n,L))
then u = p by TARSKI:def 1;
hence u in the carrier of (Polynom-Ring (n,L)) by POLYNOM1:def 11; :: thesis: verum

end;

hence {p} is Subset of (Polynom-Ring (n,L)) by TARSKI:def 3; :: thesis: verum