defpred S₁[ set , set ] means ex p, q being Polynomial of n,L st
( p = $1 & q = $2 & p reduces_to q,P,T );
set A = NonZero (Polynom-Ring n,L);
set B = the carrier of (Polynom-Ring n,L);
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 A3: p reduces_to q,P,T ; :: thesis: [p,q] in R
then consider pp being Polynomial of n,L such that
pp in P and
A4: p reduces_to q,pp,T by Def7;
ex b being bag of n st p reduces_to q,pp,b,T by A4, Def6;
then p <> 0_ n,L by Def5;
then A5: not p in {(0_ n,L)} by TARSKI:def 1;
A6: q in the carrier of (Polynom-Ring n,L) by POLYNOM1:def 27;
( 0_ n,L = 0. (Polynom-Ring n,L) & p in the carrier of (Polynom-Ring n,L) ) by POLYNOM1:def 27;
then p in NonZero (Polynom-Ring n,L) by A5, XBOOLE_0:def 5;
hence [p,q] in R by A1, A3, A6; :: thesis: verum

end;

now

assume [p,q] in R ; :: thesis: p reduces_to q,P,T
then S₁[p,q] by A1;
hence p reduces_to q,P,T ; :: 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