:: deftheorem Def2 defines positive BCIALG_2:def 2 :
for X being BCI-algebra
for a being Element of X holds
( a is positive iff 0. X <= a );