:: deftheorem defines maximal BCIALG_2:def 4 :
for X being BCI-algebra
for a being Element of X holds
( a is maximal iff for x being Element of X st a <= x holds
x = a );