let X be BCI-algebra; :: thesis: ConSet X c= LConSet X

let x be object ; :: 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 ex R being Congruence of X st x = R ;

then x is L-congruence of X by Th36;

hence x in LConSet X ; :: thesis: verum

let x be object ; :: 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 ex R being Congruence of X st x = R ;

then x is L-congruence of X by Th36;

hence x in LConSet X ; :: thesis: verum