take BCI-EXAMPLE ; :: thesis: ( BCI-EXAMPLE is implicative & BCI-EXAMPLE is positive-implicative & BCI-EXAMPLE is p-Semisimple & BCI-EXAMPLE is associative & BCI-EXAMPLE is weakly-implicative & BCI-EXAMPLE is weakly-positive-implicative )
thus ( BCI-EXAMPLE is implicative & BCI-EXAMPLE is positive-implicative & BCI-EXAMPLE is p-Semisimple & BCI-EXAMPLE is associative & BCI-EXAMPLE is weakly-implicative & BCI-EXAMPLE is weakly-positive-implicative ) ; :: thesis: verum