Description: The satisfaction predicate for wff codes in the model M and the binary relation E on M is a function over suc _om . (Contributed by AV, 6-Oct-2023)