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