reconsider IT = BCI_S-EXAMPLE as BCK-Algebra_with_Condition(S) ;
IT is commutative

proof

let x, y be Element of IT; :: according to BCIALG_4:def 9 :: thesis: x \ (x \ y) = y \ (y \ x)
thus x \ (x \ y) = y \ (y \ x) by STRUCT_0:def 10; :: thesis: verum

end;

hence ex b₁ being BCK-Algebra_with_Condition(S) st b₁ is commutative ; :: thesis: verum