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

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in IConSet X or x in ConSet X )

assume x in IConSet X ; :: thesis: x in ConSet X

then ex I being Ideal of X st x is I-congruence of X,I by Def13;

hence x in ConSet X ; :: thesis: verum

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in IConSet X or x in ConSet X )

assume x in IConSet X ; :: thesis: x in ConSet X

then ex I being Ideal of X st x is I-congruence of X,I by Def13;

hence x in ConSet X ; :: thesis: verum