:: deftheorem defines ConSet BCIALG_2:def 14 :
for X being BCI-algebra holds ConSet X = { R where R is Congruence of X : verum } ;