:: deftheorem defines Red TERMORD:def 9 :
for n being Ordinal
for T being connected TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds Red (p,T) = p - (HM (p,T));