Description: The satisfaction predicate for wff codes in the model M and the binary relation E on M at an element of the successor of _om . (Contributed by AV, 22-Sep-2023)