environ
vocabularies HIDDEN, BCIALG_1, XBOOLE_0, SUBSET_1, CARD_FIL, XXREAL_0, SUPINF_2, CHORD, TARSKI, RCOMP_1, BINOP_1, STRUCT_0, WAYBEL15, BCIIDEAL;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, BCIALG_1, BCIALG_2, BCIALG_3;
definitions TARSKI, XBOOLE_0;
theorems BCIALG_1, TARSKI, XBOOLE_0, BCIALG_2, BCIALG_3;
schemes ;
registrations STRUCT_0, BCIALG_1, BCIALG_2, BCIALG_3;
constructors HIDDEN, BCIALG_2, BCIALG_3;
requirements HIDDEN, SUBSET, BOOLE;
equalities BCIALG_1;
expansions BCIALG_1, XBOOLE_0;
Lm1:
for X being BCK-algebra holds the carrier of X c= BCK-part X