for X being non empty BCIStr_1 holds
( X is positive-implicative BCK-Algebra_with_Condition(S) iff X is semi-Brouwerian-algebra )