MEMBERSHIP ::= membership TERM SORT
A membership formula is written:
T in 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.