theorem :: BCIALG_2:26

for X being BCI-algebra st 0. X is maximal holds
for a being Element of X holds a is minimal