now

let u be set ; :: 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 27; :: thesis: verum

end;

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