for MS being OrtAfPl holds
( MS is translation iff MS is satisfying_des ) by Lm3;