for X being BCI-algebra
for a being Element of X holds
( a is minimal iff ex x being Element of X st a = x ` )