let X be BCI-algebra; :: thesis: ConSet X c= RConSet X
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ConSet X or x in RConSet X )
assume x in ConSet X ; :: thesis: x in RConSet X
then ex R being Congruence of X st x = R ;
then x is R-congruence of X by Th36;
hence x in RConSet X ; :: thesis: verum