A subsort declaration SUBSORT-DECL is written:

S₁, ..., S_n < S

It declares all the sorts S₁, ..., S_n, and S, as well as the embedding of each S_i as a subsort of S. The S_i must be distinct from S.

When a subsort declaration occurs in a sort generation construct, the embedding and projection operations between the subsort(s) and the supersort are treated as declared operations with regard to generation of sorts. Introducing an embedding relation between two sorts may cause operation symbols to become related by the overloading relation, so that values of terms become equated when the terms are identical up to embedding.