A subsort definition SUBSORT-DEFN is written:

S = { V:S'   ·   F }

It provides an explicit specification of the values of the subsort S of S', in contrast to the implicit specification provided by using subsort declarations and overloaded operation symbols.

The subsort definition declares the sort S; it declares the embedding of S as a subsort of S', which must already be declared in the local environment; and it asserts that the values of S are precisely (the projection of) those values of the variable V from S' for which the formula F holds.

The scope of the variable V is restricted to the formula F. Any other variables occurring in F must be explicitly declared by enclosing quantifications.

Note that the terms of sort S' cannot generally be used as terms of sort S. But they can be explicitly projected to S, using a cast.