∀x (x∈G ↔ x∈DJ)