record convergent_generated_topology : Type ≝
{ AA:> axiom_set;
convergence: ∀a:AA.∀U,V:Ω \sup AA. a ◃ U → a ◃ V → a ◃ (U ↓ V)
}.
record convergent_generated_topology : Type ≝
{ AA:> axiom_set;
convergence: ∀a:AA.∀U,V:Ω \sup AA. a ◃ U → a ◃ V → a ◃ (U ↓ V)
}.