---

Step * of Lemma sub-system_transitivity

∀[M:Type ─→ Type]
  ∀S1,S2,S3:System(P.M[P]).  (sub-system(P.M[P];S1;S2) ⇒ sub-system(P.M[P];S2;S3) ⇒ sub-system(P.M[P];S1;S3))
BY
{ ((D 0 THENA Auto)
   THEN RepeatFor 3 (((D 0 THENA Auto) THEN D -1))
   THEN RepUR ``sub-system`` 0
   THEN Auto
   THEN ( (InstLemma `sublist_transitivity` [])⋅ THEN Auto)
   THEN  (InstLemma `lg-contains_transitivity` [])⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}S1,S2,S3:System(P.M[P]).
        (sub-system(P.M[P];S1;S2)  {}\mRightarrow{}  sub-system(P.M[P];S2;S3)  {}\mRightarrow{}  sub-system(P.M[P];S1;S3))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  RepeatFor  3  (((D  0  THENA  Auto)  THEN  D  -1))
  THEN  RepUR  ``sub-system``  0
  THEN  Auto
  THEN  (  (InstLemma  `sublist\_transitivity`  [])\mcdot{}  THEN  Auto)
  THEN    (InstLemma  `lg-contains\_transitivity`  [])\mcdot{}
  THEN  Auto)

---

Home Index