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