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