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