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