theorem :: NEWTON07:72

RHartr 1 = <*1*> by NC0;