Step
*
1
1
of Lemma
ss-eq_transitivity
1. ss : SeparationSpace
2. x : Point
3. y : Point
4. z : Point
5. ¬x # y
6. ¬y # z
7. x # z
8. z # y
⊢ False
BY
{ (D -3 THEN EAuto 1) }
Latex:
Latex:
1.  ss  :  SeparationSpace
2.  x  :  Point
3.  y  :  Point
4.  z  :  Point
5.  \mneg{}x  \#  y
6.  \mneg{}y  \#  z
7.  x  \#  z
8.  z  \#  y
\mvdash{}  False
By
Latex:
(D  -3  THEN  EAuto  1)
Home
Index