set M = { (S-Poly p1,p2,T) where p1, p2 is Polynomial of n,L : ( p1 in P & p2 in P ) } ;

now

let u be set ; :: thesis: ( u in { (S-Poly p1,p2,T) where p1, p2 is Polynomial of n,L : ( p1 in P & p2 in P ) } implies u in the carrier of (Polynom-Ring n,L) )
assume u in { (S-Poly p1,p2,T) where p1, p2 is Polynomial of n,L : ( p1 in P & p2 in P ) } ; :: thesis: u in the carrier of (Polynom-Ring n,L)
then ex p1, p2 being Polynomial of n,L st
( u = S-Poly p1,p2,T & p1 in P & p2 in P ) ;
hence u in the carrier of (Polynom-Ring n,L) by POLYNOM1:def 27; :: thesis: verum

end;

hence { (S-Poly p1,p2,T) where p1, p2 is Polynomial of n,L : ( p1 in P & p2 in P ) } is Subset of (Polynom-Ring n,L) by TARSKI:def 3; :: thesis: verum