theorem Ch7: :: ABSRED_0:95

for X being ARS st X is SN holds
the reduction of X is strongly-normalizing