---

Step * of Lemma bag-maximals-max

∀[T:Type]. ∀[b:bag(T)]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[x,y:T].  (↑(R x y)) supposing (x ↓∈ bag-maximals(b;R) and y ↓∈ b)
BY
{ ((UnivCD THENA Auto)
   THEN (BagToList 2 THENA Auto)
   THEN BagMemberD (-1)
   THEN Auto
   THEN FLemma `bag-maximal?-max` [-3;-1]
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[b:bag(T)].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[x,y:T].
    (\muparrow{}(R  x  y))  supposing  (x  \mdownarrow{}\mmember{}  bag-maximals(b;R)  and  y  \mdownarrow{}\mmember{}  b)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (BagToList  2  THENA  Auto)
  THEN  BagMemberD  (-1)
  THEN  Auto
  THEN  FLemma  `bag-maximal?-max`  [-3;-1]
  THEN  Auto)

---

Home Index