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

let u be object ; :: 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 :: thesis: ( ( u = p & u in the carrier of (Polynom-Ring (n,L)) ) or ( u = q & u in the carrier of (Polynom-Ring (n,L)) ) )

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 11; :: 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 11; :: 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