 Solution

Absorb (4) using the equivalenceThus we can takeHere $A⊑\neg B$ is a primitive inclusion, handled by adding $\neg B$ whenever $A$ labels a node. For literal substitution-based TBox unfolding, introduce a fresh description logic concept $A_0$ and replace the primitive inclusion byThis preserves the original models after forgetting $A_0$: any model of the primitive inclusion extends by taking $A_0=A$, and any model of the new definition satisfies the primitive inclusion. The fresh name is important. Replacing $A$ by $\neg B$ alone would incorrectly assert that every non-$B$ element is an $A$ element.