The inclusion relation. Like equality, it is formed by a binary relation symbol, thus defined on the entire class universe. If A ⊆ B, then we say that A is included in B, or that A is a subclass of B. Inclusion is a partial order on the class universe, as incl_refl, incl_trans and incl_antisym show.