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

now :: thesis: for u being object st u in { (S-Poly (p1,p2,T)) where p1, p2 is Polynomial of n,L : ( p1 in P & p2 in P ) } holds
u in the carrier of (Polynom-Ring (n,L))

let u be object ; :: 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 11; :: 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