for X being BCI-algebra st ex x being Element of X st x is greatest holds
for a being Element of X holds a is positive