MEMBERSHIP ::= membership TERM SORT
A membership formula is written:
T e sThe sign displayed as the set-membership symbol in LaTeX is input as `in'.
It is well-sorted if the term T is well-sorted for a supersort s' of the specified sort s. It expands to an application of the pre-declared predicate symbol for testing s' values for membership in the embedding of s.