set A = NonZero (Polynom-Ring n,L);
set B = the carrier of (Polynom-Ring n,L);
defpred S₁[ set , set ] means ex p, q being Polynomial of n,L st
( p = $1 & q = $2 & p reduces_to q,P,T );
consider R being Relation of (NonZero (Polynom-Ring n,L)),the carrier of (Polynom-Ring n,L) such that
A1: for x, y being set holds
( [x,y] in R iff ( x in NonZero (Polynom-Ring n,L) & y in the carrier of (Polynom-Ring n,L) & S₁[x,y] ) ) from RELSET_1:sch 1();
take R ; :: thesis: for p, q being Polynomial of n,L holds
( [p,q] in R iff p reduces_to q,P,T )

now

let p, q be Polynomial of n,L; :: thesis: ( [p,q] in R iff p reduces_to q,P,T )

A2: now

assume [p,q] in R ; :: thesis: p reduces_to q,P,T
then ( p in NonZero (Polynom-Ring n,L) & q in the carrier of (Polynom-Ring n,L) & S₁[p,q] ) by A1;
hence p reduces_to q,P,T ; :: thesis: verum

end;

now

assume A3: p reduces_to q,P,T ; :: thesis: [p,q] in R
then consider pp being Polynomial of n,L such that
A4: ( pp in P & p reduces_to q,pp,T ) by Def7;
consider b being bag of such that
A5: p reduces_to q,pp,b,T by A4, Def6;
X: 0_ n,L = 0. (Polynom-Ring n,L) by POLYNOM1:def 27;
p <> 0_ n,L by A5, Def5;
then A6: not p in {(0_ n,L)} by TARSKI:def 1;
p in the carrier of (Polynom-Ring n,L) by POLYNOM1:def 27;
then ( p in NonZero (Polynom-Ring n,L) & q in the carrier of (Polynom-Ring n,L) ) by A6, X, POLYNOM1:def 27, XBOOLE_0:def 5;
hence [p,q] in R by A1, A3; :: thesis: verum

end;

hence ( [p,q] in R iff p reduces_to q,P,T ) by A2; :: thesis: verum

end;

hence for p, q being Polynomial of n,L holds
( [p,q] in R iff p reduces_to q,P,T ) ; :: thesis: verum