:: deftheorem defines COMP ABSRED_0:def 28 :
for X being ARS holds
( X is COMP iff ( X is SN & X is CONF ) );