Definition (TBox). A TBox T is a finite collection of concept inclusion axioms of the form C ⊑ D and concept equivalence axioms of the form C ≡ D, where C and D are concepts.
