theorem ThSN: :: ABSRED_0:97

for X being ARS holds
( X is SN iff for A being set
for z being Element of X holds
( not z in A or ex x being Element of X st
( x in A & ( for y being Element of X holds
( not y in A or not x ==> y ) ) ) ) )