:: deftheorem defines is_top_reducible_wrt POLYRED:def 12 :
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f being Polynomial of n,L
for P being Subset of (Polynom-Ring (n,L)) holds
( f is_top_reducible_wrt P,T iff ex p being Polynomial of n,L st
( p in P & f is_top_reducible_wrt p,T ) );