Updating instances of `ae` and `near` notations

[hoheinzollern]

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).