---

Step * 1 of Lemma ss-sep-symmetry


1. ss : SeparationSpace
2. x : Point(ss)
3. y : Point(ss)
4. x # y
5. x # x
⊢ y # x
BY
{ (InstLemma `ss-sep-irrefl` [⌜ss⌝;⌜x⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  ss  :  SeparationSpace
2.  x  :  Point(ss)
3.  y  :  Point(ss)
4.  x  \#  y
5.  x  \#  x
\mvdash{}  y  \#  x


By

---

Latex:
(InstLemma  `ss-sep-irrefl`  [\mkleeneopen{}ss\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index