let X be BCI-algebra; :: thesis: IConSet X c= ConSet X
let x be set ; :: 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 consider I being Ideal of X such that
A1: x is I-congruence of X,I by Def13;
thus x in ConSet X by A1; :: thesis: verum