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