take BCI-EXAMPLE ; :: thesis: BCI-EXAMPLE is commutative
thus BCI-EXAMPLE is commutative ; :: thesis: verum