fixed pictures

[helm.git] / helm / software / matita / nlibrary / topology / cantor.ma

diff --git a/helm/software/matita/nlibrary/topology/cantor.ma b/helm/software/matita/nlibrary/topology/cantor.ma
index b8f8a5543ad57e8cf24ea8ee2f169e63ac94c0aa..6ae8d36ad299078b76670460b6b3a0a16016faf3 100644 (file)
--- a/helm/software/matita/nlibrary/topology/cantor.ma
+++ b/helm/software/matita/nlibrary/topology/cantor.ma
@@ -28,6 +28,7 @@ interpretation "empty" 'empty = (emptyset ?).
 
 naxiom EM : ∀A:Ax.∀a:A.∀i_star.(a ∈ 𝐂 a i_star) ∨ ¬( a ∈ 𝐂 a i_star).
 
+alias symbol "covers" = "covers".
 ntheorem th2_3 :
   ∀A:Ax.∀a:A. a ◃ ∅ → ∃i. ¬ a ∈ 𝐂 a i.
 #A; #a; #H; nelim H;
@@ -130,6 +131,7 @@ naxiom h : nat → nat.
 alias symbol "eq" = "leibnitz's equality".
 alias symbol "eq" = "setoid1 eq".
 alias symbol "covers" = "covers".
+alias symbol "eq" = "leibnitz's equality".
 naxiom Ph :  ∀x.h x = O \liff  x ◃ ∅.
 
 nlemma replace_char: