Incorrect answer for LargestTwinPair exercise

[pshirshov]

LargestTwinPairRef(S) == CHOOSE <<x, y>> \in S \X S:
                         /\ IsPrime(x)
                         /\ IsPrime(y)
                         /\ x = y - 2
                         /\ \A <<w, z>> \in S \X S:
                            /\ IsPrime(z)
                            /\ IsPrime(w)
                            /\ w = z - 2
                            => z < y

PrintVal(id, exp)  ==  Print(<<id, exp>>, TRUE)
ASSUME PrintVal("LargestTwinPairRef", LargestTwinPairRef({3, 5, 13}))

(see https://learntla.com/tla/logic/)

Produces

Evaluating assumption line 72, col 8 to line 72, col 54 of module hw failed.
Attempted to compute the value of an expression of form
CHOOSE x \in S: P, but no element of S satisfied P.
line 54, col 25 to line 62, col 36 of module hw

It should be z <= y