theorem :: BCIALG_3:12

for X being BCI-algebra st ex a being Element of X st a is being_greatest holds
X is BCK-algebra