∀u∀w∀x∀y∀z(((G(w,u)&G(x,u))&(G(y,u)&G(z,u)))->(((w=xvw=y)vw=z)v((x=yvx=z)vy=z)))

Where G(x,y) is a propositional function meaning "x is the grandmother of y," and the domain for all variable consists of the set of all people.

I figured I would write the negation of the statement "Someone has more than three grandmothers," i.e.,

~∃u∃w∃x∃y∃z(((Gwu&Gxu)&(Gyu&Gzu))&(((w≠x&w≠y)&w≠z)&((x≠y&x≠z)&y≠z)))

and then just move the ~ in until I got the above universal quantification. But is there a simpler way to express the proposition?