now

let u be set ; :: thesis: ( u in {p,q} implies u in the carrier of (Polynom-Ring n,L) )
assume A1: u in {p,q} ; :: thesis: u in the carrier of (Polynom-Ring n,L)

now

per cases ( u = p or u = q ) by A1, TARSKI:def 2;

case u = p ; :: thesis: u in the carrier of (Polynom-Ring n,L)

hence u in the carrier of (Polynom-Ring n,L) by POLYNOM1:def 27; :: thesis: verum

end;

case u = q ; :: thesis: u in the carrier of (Polynom-Ring n,L)

hence u in the carrier of (Polynom-Ring n,L) by POLYNOM1:def 27; :: thesis: verum

end;

end;

end;

hence u in the carrier of (Polynom-Ring n,L) ; :: thesis: verum

end;

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