now :: thesis: for u being object st u in {p} holds

u in the carrier of (Polynom-Ring (n,L))

hence
{p} is Subset of (Polynom-Ring (n,L))
by TARSKI:def 3; :: thesis: verumu 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;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