for X being BCK-Algebra_with_Condition(S) holds
( X is implicative iff ( X is commutative & X is positive-implicative ) )