Before Lemma 2: T
≤M
should read SN(>
spo
)
≤M