theorem :: ABSRED_0:114

ex X being ARS st
( X is WN & not X is SN )