theorem Ch8: :: ABSRED_0:96

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