:: deftheorem defines SN ABSRED_0:def 15 :
for X being ARS holds
( X is SN iff for f being Function of NAT, the carrier of X holds
not for i being Nat holds f . i ==> f . (i + 1) );