Step * 1 1 of Lemma dM-0-not-1


1. fset(ℕ)
⊢ ¬(0 1 ∈ Point(free-DeMorgan-lattice(names(I);NamesDeq)))
BY
((Subst' THENA (RW (SubC (SymbCompC [] 100)) THEN Auto))
   THEN (Subst' THENA (RW (SubC (SymbCompC [] 100)) THEN Auto))
   }

1
1. fset(ℕ)
⊢ ¬(0 1 ∈ Point(free-DeMorgan-lattice(names(I);NamesDeq)))


Latex:


Latex:

1.  I  :  fset(\mBbbN{})
\mvdash{}  \mneg{}(0  =  1)


By


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




Home Index