+qed.
+
+theorem covers_elim2:
+ ∀A: axiom_set. ∀U:Ω \sup A.∀P: A → CProp.
+ (∀a:A. a ∈ U → P a) →
+ (∀a:A.∀V:Ω \sup A. a ◃ V → V ◃ U → (∀y. y ∈ V → P y) → P a) →
+ ∀a:A. a ◃ U → P a.
+ intros;
+ change with (a ∈ {a | P a});
+ apply (covers_elim ?????? H2);
+ [ intros 2; simplify; apply H; assumption
+ | intros;
+ simplify in H4 ⊢ %;
+ apply H1;
+ [ apply (C ? a1 j);
+ | autobatch;
+ | assumption;
+ | assumption]]
+qed.
+
+theorem coreflexivity: ∀A:axiom_set.∀a:A.∀V. a ⋉ V → a ∈ V.
+ intros;
+ cases H;
+ assumption.
+qed.
+
+theorem cotransitivity:
+ ∀A:axiom_set.∀a:A.∀U,V. a ⋉ U → (∀b:A. b ⋉ U → b ∈ V) → a ⋉ V.
+ intros;
+ apply (fish_rec ?? {a|a ⋉ U} ??? H); simplify; intros;
+ [ apply H1; apply H2;
+ | cases H2 in j; clear H2; intro i;
+ cases (H4 i); clear H4; exists[apply a3] assumption]
+qed.
+
+theorem compatibility: ∀A:axiom_set.∀a:A.∀U,V. a ⋉ V → a ◃ U → U ⋉ V.
+ intros;
+ generalize in match H; clear H;
+ apply (covers_elim ?? {a|a ⋉ V → U ⋉ V} ??? H1);
+ clear H1; simplify; intros;
+ [ exists [apply x] assumption
+ | cases H2 in j H H1; clear H2 a1; intros;
+ cases (H1 i); clear H1; apply (H3 a1); assumption]
+qed.
+
+definition leq ≝ λA:axiom_set.λa,b:A. a ◃ {y|b=y}.
+
+interpretation "covered by one" 'leq a b = (leq ? a b).
+
+theorem leq_refl: ∀A:axiom_set.∀a:A. a ≤ a.
+ intros;
+ apply refl;
+ normalize;
+ reflexivity.
+qed.
+
+theorem leq_trans: ∀A:axiom_set.∀a,b,c:A. a ≤ b → b ≤ c → a ≤ c.
+ intros;
+ unfold in H H1 ⊢ %;
+ apply (transitivity ???? H);
+ constructor 1;
+ intros;
+ normalize in H2;
+ rewrite < H2;
+ assumption.
+qed.
+
+definition uparrow ≝ λA:axiom_set.λa:A.mk_powerset ? (λb:A. a ≤ b).
+
+interpretation "uparrow" 'uparrow a = (uparrow ? a).
+
+definition downarrow ≝ λA:axiom_set.λU:Ω \sup A.mk_powerset ? (λa:A. (↑a) ≬ U).
+
+interpretation "downarrow" 'downarrow a = (downarrow ? a).
+
+definition fintersects ≝ λA:axiom_set.λU,V:Ω \sup A.↓U ∩ ↓V.
+
+interpretation "fintersects" 'fintersects U V = (fintersects ? U V).
+
+record convergent_generated_topology : Type ≝
+ { AA:> axiom_set;
+ convergence: ∀a:AA.∀U,V:Ω \sup AA. a ◃ U → a ◃ V → a ◃ (U ↓ V)
+ }.