---

Step * 1 1 of Lemma approx-per-trans


1. [T] : Type
2. a : Base
3. b : Base
4. c : Base
5. t3 : Base
6. a ≤ t3
7. t3 ∈ T
8. t2 : Base
9. b ≤ t2
10. t2 ∈ T
11. ∀t:Base. (((a ≤ t) ∧ (t ∈ T)) ⇒ (∃t':Base. ((b ≤ t') ∧ (t' = t ∈ T))))
12. ∀t:Base. (((b ≤ t) ∧ (t ∈ T)) ⇒ (∃t':Base. ((a ≤ t') ∧ (t' = t ∈ T))))
13. t1 : Base
14. b ≤ t1
15. t1 ∈ T
16. t : Base
17. c ≤ t
18. t ∈ T
19. ∀t:Base. (((b ≤ t) ∧ (t ∈ T)) ⇒ (∃t':Base. ((c ≤ t') ∧ (t' = t ∈ T))))
20. ∀t:Base. (((c ≤ t) ∧ (t ∈ T)) ⇒ (∃t':Base. ((b ≤ t') ∧ (t' = t ∈ T))))
21. t4 : Base
22. (a ≤ t4) ∧ (t4 ∈ T)
23. t' : Base
24. (b ≤ t') ∧ (t' = t4 ∈ T)
⊢ ∃t':Base. ((c ≤ t') ∧ (t' = t4 ∈ T))
BY
{ OnMaybeHyp 19 (\h. ((InstHyp [⌜t'⌝] h⋅ THENA Complete (Auto)) THEN ParallelLast THEN Complete (Auto))) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  a  :  Base
3.  b  :  Base
4.  c  :  Base
5.  t3  :  Base
6.  a  \mleq{}  t3
7.  t3  \mmember{}  T
8.  t2  :  Base
9.  b  \mleq{}  t2
10.  t2  \mmember{}  T
11.  \mforall{}t:Base.  (((a  \mleq{}  t)  \mwedge{}  (t  \mmember{}  T))  {}\mRightarrow{}  (\mexists{}t':Base.  ((b  \mleq{}  t')  \mwedge{}  (t'  =  t))))
12.  \mforall{}t:Base.  (((b  \mleq{}  t)  \mwedge{}  (t  \mmember{}  T))  {}\mRightarrow{}  (\mexists{}t':Base.  ((a  \mleq{}  t')  \mwedge{}  (t'  =  t))))
13.  t1  :  Base
14.  b  \mleq{}  t1
15.  t1  \mmember{}  T
16.  t  :  Base
17.  c  \mleq{}  t
18.  t  \mmember{}  T
19.  \mforall{}t:Base.  (((b  \mleq{}  t)  \mwedge{}  (t  \mmember{}  T))  {}\mRightarrow{}  (\mexists{}t':Base.  ((c  \mleq{}  t')  \mwedge{}  (t'  =  t))))
20.  \mforall{}t:Base.  (((c  \mleq{}  t)  \mwedge{}  (t  \mmember{}  T))  {}\mRightarrow{}  (\mexists{}t':Base.  ((b  \mleq{}  t')  \mwedge{}  (t'  =  t))))
21.  t4  :  Base
22.  (a  \mleq{}  t4)  \mwedge{}  (t4  \mmember{}  T)
23.  t'  :  Base
24.  (b  \mleq{}  t')  \mwedge{}  (t'  =  t4)
\mvdash{}  \mexists{}t':Base.  ((c  \mleq{}  t')  \mwedge{}  (t'  =  t4))


By

---

Latex:
OnMaybeHyp  19  (\mbackslash{}h.  ((InstHyp  [\mkleeneopen{}t'\mkleeneclose{}]  h\mcdot{}  THENA  Complete  (Auto))
                                        THEN  ParallelLast
                                        THEN  Complete  (Auto)))

---

Home Index