Step * 1 of Lemma alle-at-iff


1. es EO@i'
2. Id@i
3. [P] {e:E| loc(e) i ∈ Id}  ─→ ℙ
4. ∀e@i.P[e]@i
⊢ ∀e@i.P[e] supposing ↑first(e)
BY
((RepeatFor ((ParallelOp (-1))))⋅ THEN Auto) }


Latex:



1.  es  :  EO@i'
2.  i  :  Id@i
3.  [P]  :  \{e:E|  loc(e)  =  i\}    {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}e@i.P[e]@i
\mvdash{}  \mforall{}e@i.P[e]  supposing  \muparrow{}first(e)


By

((RepeatFor  3  ((ParallelOp  (-1))))\mcdot{}  THEN  Auto)




Home Index