environ
vocabularies HIDDEN, XBOOLE_0, BCIALG_1, BINOP_1, SUBSET_1, XXREAL_0, SUPINF_2, XXREAL_2, CARD_FIL, BCIALG_3;
notations HIDDEN, XBOOLE_0, SUBSET_1, STRUCT_0, BCIALG_1;
definitions ;
theorems BCIALG_1, STRUCT_0;
schemes ;
registrations STRUCT_0, BCIALG_1;
constructors HIDDEN, BCIALG_1;
requirements HIDDEN, SUBSET;
equalities BCIALG_1;
expansions BCIALG_1;
Lm1:
for X being bounded BCK-algebra st X is BCK-implicative holds
for a being Element of X st a is being_greatest holds
for x being Element of X holds a \ (a \ x) = x