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