Description: Extend wff notation to include the strict total ordering predicate. Read: " R orders A ".