theorem :: BCIALG_5:44
for X being BCI-algebra st X is associative BCI-algebra holds
( X is BCI-algebra of 0 ,1, 0 , 0 & X is BCI-algebra of 1, 0 , 0 , 0 )