:: deftheorem defines Hartr NEWTON07:def 2 :
for n being non zero Nat holds Hartr n = (RHartr n) " ;