let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds Support (Red (p,T)) c= Support p
let O be connected TermOrder of n; :: thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds Support (Red (p,O)) c= Support p
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of n,L holds Support (Red (p,O)) c= Support p
let p be Polynomial of n,L; :: thesis: Support (Red (p,O)) c= Support p
Support (Red (p,O)) = (Support p) \ {(HT (p,O))} by Lm17;
hence Support (Red (p,O)) c= Support p by XBOOLE_1:36; :: thesis: verum