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)) ; :: thesis: verum