add references to Egbert's theorem, and simplify some quantifiers
by putting them into words