---

Step * 1 of Lemma ex-approx-context


1. e : Atom2
2. a : Base
3. b : Base
4. g : Base
5. e#g:Base
6. ex-approx(e;a;b)
⊢ ex-approx(e;g a;g b)
BY
{ (ParallelLast THEN RepeatFor 2 (D 0 THENA Auto⋅)) }

1
1. e : Atom2
2. a : Base
3. b : Base
4. g : Base
5. e#g:Base
6. ∀f:Base. (e#f:Base ⇒ (f a?e:v.⊥ ≤ f b?e:v.⊥))
7. f : Base
8. e#f:Base
⊢ f (g a)?e:v.⊥ ≤ f (g b)?e:v.⊥

---

Latex:

---

Latex:

1.  e  :  Atom2
2.  a  :  Base
3.  b  :  Base
4.  g  :  Base
5.  e\#g:Base
6.  ex-approx(e;a;b)
\mvdash{}  ex-approx(e;g  a;g  b)


By

---

Latex:
(ParallelLast  THEN  RepeatFor  2  (D  0  THENA  Auto\mcdot{}))

---

Home Index