:: deftheorem defines RConSet BCIALG_2:def 16 :
for X being BCI-algebra holds RConSet X = { R where R is R-congruence of X : verum } ;