5.532

And analogously: not “ ( ∃ x , y ) . f ⁡ ( x , y ) . x = y ”, but “ ( ∃ x )

471