let X be BCI-algebra; :: thesis: ConSet X c= LConSet X
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ConSet X or x in LConSet X )
assume x in ConSet X ; :: thesis: x in LConSet X
then consider R being Congruence of X such that
A1: x = R ;
x is L-congruence of X by A1, Th36;
hence x in LConSet X ; :: thesis: verum