reconsider IT = BCI_S-EXAMPLE as BCK-Algebra_with_Condition(S) ;
IT is positive-implicative by STRUCT_0:def 10;
hence ex b₁ being BCK-Algebra_with_Condition(S) st b₁ is positive-implicative ; :: thesis: verum