---

Step * 1 of Lemma face-lattice-0-not-1


1. J : fset(ℕ)
2. 0 = 1 ∈ Point(face_lattice(J))
⊢ False
BY
{ ((Subst' 0 ~ {} -1 THENA (RW (SubC (SymbCompC [] 100)) 0 THEN Auto))
   THEN (Subst' 1 ~ {{}} -1 THENA (RW (SubC (SymbCompC [] 100)) 0 THEN Auto))
   ) }

1
1. J : fset(ℕ)
2. {} = {{}} ∈ Point(face_lattice(J))
⊢ False

---

Latex:

---

Latex:

1.  J  :  fset(\mBbbN{})
2.  0  =  1
\mvdash{}  False


By

---

Latex:
((Subst'  0  \msim{}  \{\}  -1  THENA  (RW  (SubC  (SymbCompC  []  100))  0  THEN  Auto))
  THEN  (Subst'  1  \msim{}  \{\{\}\}  -1  THENA  (RW  (SubC  (SymbCompC  []  100))  0  THEN  Auto))
  )

---

Home Index