take BCI-EXAMPLE ; :: thesis: ( BCI-EXAMPLE is Iseki_extension & BCI-EXAMPLE is BCK-positive-implicative & BCI-EXAMPLE is BCK-implicative & BCI-EXAMPLE is bounded & BCI-EXAMPLE is commutative )
thus ( BCI-EXAMPLE is Iseki_extension & BCI-EXAMPLE is BCK-positive-implicative & BCI-EXAMPLE is BCK-implicative & BCI-EXAMPLE is bounded & BCI-EXAMPLE is commutative ) ; :: thesis: verum