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