Step * 1 of Lemma es-causl_transitivity2


1. es EO@i'
2. E@i
3. E@i
4. E@i
5. (x < y)@i
6. (y < z)@i
⊢ (x < z)
BY
((Using [`y',⌜y⌝(BLemma `es-causl_transitivity`))⋅ THEN Auto) }


Latex:


Latex:

1.  es  :  EO@i'
2.  x  :  E@i
3.  y  :  E@i
4.  z  :  E@i
5.  (x  <  y)@i
6.  (y  <  z)@i
\mvdash{}  (x  <  z)


By


Latex:
((Using  [`y',\mkleeneopen{}y\mkleeneclose{}]  (BLemma  `es-causl\_transitivity`))\mcdot{}  THEN  Auto)




Home Index