set IT = BCI-EXAMPLE ;
thus BCI-EXAMPLE is BCK-positive-implicative :: thesis: BCI-EXAMPLE is BCK-implicative

proof

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

end;

let x, y be Element of BCI-EXAMPLE ; :: according to BCIALG_3:def 12 :: thesis: x \ (y \ x) = x
thus x \ (y \ x) = x by STRUCT_0:def 10; :: thesis: verum