Updating instances of ae and near notations #1617
Description
The discussion in #1600 shows that the {ae mu, P} notation is used in places where \forall x \ae mu, Q x should be preferred (where P = forall x, Q x).
We should review all instances of ae and near to check that {ae and {near are used only when an existing statement is being relativised. Otherwise prefer \forall x \ae mu and \forall x \near F, respectively.
Additionally, we should consider equivalent notation for in (i.e. introduce \forall x \in D, P x to match the {in D, P} notation and check all instances).