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