take BCI-EXAMPLE ; :: thesis: ( BCI-EXAMPLE is strict & BCI-EXAMPLE is being_B & BCI-EXAMPLE is being_C & BCI-EXAMPLE is being_I & BCI-EXAMPLE is being_BCI-4 & BCI-EXAMPLE is being_BCK-5 )
thus ( BCI-EXAMPLE is strict & BCI-EXAMPLE is being_B & BCI-EXAMPLE is being_C & BCI-EXAMPLE is being_I & BCI-EXAMPLE is being_BCI-4 & BCI-EXAMPLE is being_BCK-5 ) ; :: thesis: verum