The local model checking tree has a loop on nodes 4->5->6->7->8->9->4 where nodes 4 and 7 contain fixpoint formulas with a greatest fixpoint. The outermost fixpoint of the loop does therefore not cover a least fixpoint formula (in that case it would be false), but a greatest one, so it is true.

Don't be confused; the mentioned greatest fixpoint is contained in a least fixpoint that is found in nodes 1 and 15. The nodes 1 and 15 expose the greatest fixpoints in nodes 4 and 7, but neither node 1 nor node 15 is on the mentioned loop.