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

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

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