notation "1" with precedence 89
for @{ 'unit }.
-interpretation "Unit" 'unit =
- cic:/matita/formal_topology/one.con.
+interpretation "Unit" 'unit = one.
axiom one_left: ∀A. 1 A = A.
axiom one_right: ∀A:S. A 1 = A.
notation "hvbox(A break ⊆ B)" with precedence 59
for @{ 'subseteq $A $B}.
-interpretation "Subseteq" 'subseteq A B =
- (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ A
- (cic:/matita/formal_topology/comp.con
- cic:/matita/formal_topology/eps.con B)).
+interpretation "Subseteq" 'subseteq A B = (eq _ A (comp eps B)).
axiom leq_refl: ∀A. A ⊆ A.
axiom leq_antisym: ∀A,B. A ⊆ B → B ⊆ A → A=B.
theorem th5: ∀A. i (m A) = i (m (c A)). intros; auto. qed.
theorem th6: ∀A. m (i A) = c (m (i A)). intros; auto. qed.
-theorem th7: ∀A. i (m (i A)) = i (s (i A)).
\ No newline at end of file
+theorem th7: ∀A. i (m (i A)) = i (s (i A)).