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 consider p1,
p2 being
Polynomial of
n,
L such that A1:
(
u = S-Poly p1,
p2,
T &
p1 in P &
p2 in P )
;
thus
u in the
carrier of
(Polynom-Ring n,L)
by A1, 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