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