:: deftheorem defines being_greatest BCIALG_3:def 2 :
for X being BCI-algebra
for a being Element of X holds
( a is being_greatest iff for x being Element of X holds x \ a = 0. X );