thus BCI-EXAMPLE is being_B :: thesis: ( BCI-EXAMPLE is being_C & BCI-EXAMPLE is being_I & BCI-EXAMPLE is being_BCI-4 & BCI-EXAMPLE is being_BCK-5 )

proof

let x, y, z be Element of BCI-EXAMPLE; :: according to BCIALG_1:def 3 :: thesis: ((x \ y) \ (z \ y)) \ (x \ z) = 0. BCI-EXAMPLE
thus ((x \ y) \ (z \ y)) \ (x \ z) = 0. BCI-EXAMPLE by STRUCT_0:def 10; :: thesis: verum

end;

thus BCI-EXAMPLE is being_C :: thesis: ( BCI-EXAMPLE is being_I & BCI-EXAMPLE is being_BCI-4 & BCI-EXAMPLE is being_BCK-5 )

proof

let x, y, z be Element of BCI-EXAMPLE; :: according to BCIALG_1:def 4 :: thesis: ((x \ y) \ z) \ ((x \ z) \ y) = 0. BCI-EXAMPLE
thus ((x \ y) \ z) \ ((x \ z) \ y) = 0. BCI-EXAMPLE by STRUCT_0:def 10; :: thesis: verum

end;

thus BCI-EXAMPLE is being_I :: thesis: ( BCI-EXAMPLE is being_BCI-4 & BCI-EXAMPLE is being_BCK-5 )

proof

let x be Element of BCI-EXAMPLE; :: according to BCIALG_1:def 5 :: thesis: x \ x = 0. BCI-EXAMPLE
thus x \ x = 0. BCI-EXAMPLE by STRUCT_0:def 10; :: thesis: verum

end;

thus BCI-EXAMPLE is being_BCI-4 :: thesis: BCI-EXAMPLE is being_BCK-5

proof

let x, y be Element of BCI-EXAMPLE; :: according to BCIALG_1:def 7 :: thesis: ( x \ y = 0. BCI-EXAMPLE & y \ x = 0. BCI-EXAMPLE implies x = y )
thus ( x \ y = 0. BCI-EXAMPLE & y \ x = 0. BCI-EXAMPLE implies x = y ) by STRUCT_0:def 10; :: thesis: verum

end;

for x being Element of BCI-EXAMPLE holds x ` = 0. BCI-EXAMPLE by STRUCT_0:def 10;
hence BCI-EXAMPLE is being_BCK-5 by Def8; :: thesis: verum