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;
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: