---

Step * of Lemma ss-sep-irrefl

∀[ss:SeparationSpace]. ∀[x:Point].  (¬x # x)
BY
{ (Auto THEN D 1 THEN Auto THEN Unfold `ss-sep` 0) }

1
1. ss : self:"Point":Type
        "#":{s:self."Point" ⟶ self."Point" ⟶ ℙ| ∀x:self."Point". (¬(s x x))} 
        "#symm":∀x,y:self."Point".  ((self."#" x y) ⇒ (self."#" y x)) ⋂ x:Atom ⟶ if x =a "#or"
                                                                                   then ∀x,y,z:self."Point".
                                                                                          ((self."#" x y)
                                                                                          ⇒ ((self."#" x z)
                                                                                             ∨ (self."#" y z)))
                                                                                   else Top
                                                                                   fi 
2. ss ∈ record(x.Top)
3. x : Point
4. ss."Point" ∈ Type
5. ss."#" ∈ {s:ss."Point" ⟶ ss."Point" ⟶ ℙ| ∀x:ss."Point". (¬(s x x))} 
6. ss."#symm" ∈ ∀x,y:ss."Point".  ((ss."#" x y) ⇒ (ss."#" y x))
7. ss."#or" ∈ ∀x,y,z:ss."Point".  ((ss."#" x y) ⇒ ((ss."#" x z) ∨ (ss."#" y z)))
⊢ ¬(ss."#" x x)

---

Latex:

---

Latex:
\mforall{}[ss:SeparationSpace].  \mforall{}[x:Point].    (\mneg{}x  \#  x)


By

---

Latex:
(Auto  THEN  D  1  THEN  Auto  THEN  Unfold  `ss-sep`  0)

---

Home Index