|Description: Extend the definition of
a wff to include the "defined at" predicate.
Read: "(the function) 𝐹 is defined at (the argument) 𝐴".
previous version, the token "def@" was used. However, since the
@ is used
(informally) as a replacement for $ in commented out sections that may be
deleted some day. While there is no violation of any standard to use the
@ in a token, it could make the search for such commented-out sections
slightly more difficult. (See remark of Norman Megill at