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