Step * of Lemma es-p-locl_transitivity2

es:EO. ∀p:E ⟶ (E Top). ∀a,b,c:E.  (a p≤  p<  p< c)
BY
((Unfold `es-p-le` THEN Auto) THEN SplitOrHyps) }

1
1. es EO@i'
2. E ⟶ (E Top)@i
3. E@i
4. E@i
5. E@i
6. p< b@i
7. p< c@i
⊢ p< c

2
1. es EO@i'
2. E ⟶ (E Top)@i
3. E@i
4. E@i
5. E@i
6. b ∈ E@i
7. p< c@i
⊢ p< c


Latex:


Latex:
\mforall{}es:EO.  \mforall{}p:E  {}\mrightarrow{}  (E  +  Top).  \mforall{}a,b,c:E.    (a  p\mleq{}  b  {}\mRightarrow{}  b  p<  c  {}\mRightarrow{}  a  p<  c)


By


Latex:
((Unfold  `es-p-le`  0  THEN  Auto)  THEN  SplitOrHyps)




Home Index