As for many-sorted specifications, an atomic formula is well-formed (with respect to the current declarations) if it is well-sorted and expands to a unique atomic formula for constructing sentences of the underlying institution--but now for subsorted specifications, uniqueness is required only up to an  equivalence on atomic formulae and terms. This equivalence is the least one including fully-qualified terms that are the same up to profiles of operation symbols in the overloading relation < _F and embedding, and fully-qualified atomic formulae that are the same up to the profiles of predicate symbols in the overloading relation < _P and embedding. The notions of when an atomic formula or term is well-sorted and of its expansion are indicated below for the various subsorting constructs. Due not only to overloading of predicate and/or operation symbols, but also to implicit embeddings from subsorts into supersorts, a well-sorted atomic formula or term may have several non-equivalent expansions, preventing it from being well-formed. Qualifications on operation and predicate symbols, or explicit sorts on terms, may be used to determine the intended expansion (up to the equivalence indicated above) and make it well-formed.