theorem :: BCIALG_1:44

for X being BCI-algebra holds the carrier of X is closed Ideal of X