---

Step * 1 1 of Lemma ex-approx-context


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.⊥
BY
{ (InstHyp [⌜f o g⌝] (-3)⋅ THENA Auto) }

1
.....antecedent..... 
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
⊢ e#f o g:Base

2
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
9. (f o g) a?e:v.⊥ ≤ (f o g) b?e:v.⊥
⊢ 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.  \mforall{}f:Base.  (e\#f:Base  {}\mRightarrow{}  (f  a?e:v.\mbot{}  \mleq{}  f  b?e:v.\mbot{}))
7.  f  :  Base
8.  e\#f:Base
\mvdash{}  f  (g  a)?e:v.\mbot{}  \mleq{}  f  (g  b)?e:v.\mbot{}


By

---

Latex:
(InstHyp  [\mkleeneopen{}f  o  g\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)

---

Home Index