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 10;
( 0_ (n,L) = 0. (Polynom-Ring (n,L)) & p in the carrier of (Polynom-Ring (n,L)) ) by POLYNOM1:def 10;
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