---

Step * of Lemma ss-sep-symmetry

∀ss:SeparationSpace. ∀x,y:Point(ss).  (x # y ⇒ y # x)
BY
{ (Auto THEN (InstLemma `ss-sep-or` [⌜ss⌝;⌜x⌝;⌜y⌝;⌜x⌝]⋅ THENM D -1) THEN Auto) }

1
1. ss : SeparationSpace
2. x : Point(ss)
3. y : Point(ss)
4. x # y
5. x # x
⊢ y # x

---

Latex:

---

Latex:
\mforall{}ss:SeparationSpace.  \mforall{}x,y:Point(ss).    (x  \#  y  {}\mRightarrow{}  y  \#  x)


By

---

Latex:
(Auto  THEN  (InstLemma  `ss-sep-or`  [\mkleeneopen{}ss\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENM  D  -1)  THEN  Auto)

---

Home Index