---

Step * 2 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))))
⊢ ∀t:Base. (((c ≤ t) ∧ (t ∈ T)) ⇒ (∃t':Base. ((a ≤ t') ∧ (t' = t ∈ T))))
BY
{ (ParallelLast THEN (ParallelLast THENA Auto) THEN D -1) }

1
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. (c ≤ t4) ∧ (t4 ∈ T)
23. t' : Base
24. (b ≤ t') ∧ (t' = t4 ∈ T)
⊢ ∃t':Base. ((a ≤ t') ∧ (t' = t4 ∈ T))

---

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))))
\mvdash{}  \mforall{}t:Base.  (((c  \mleq{}  t)  \mwedge{}  (t  \mmember{}  T))  {}\mRightarrow{}  (\mexists{}t':Base.  ((a  \mleq{}  t')  \mwedge{}  (t'  =  t))))


By

---

Latex:
(ParallelLast  THEN  (ParallelLast  THENA  Auto)  THEN  D  -1)

---

Home Index