take BCI-EXAMPLE ; :: thesis: ( BCI-EXAMPLE is BCI-commutative & BCI-EXAMPLE is BCI-weakly-commutative )
thus ( BCI-EXAMPLE is BCI-commutative & BCI-EXAMPLE is BCI-weakly-commutative ) ; :: thesis: verum