---

Step * of Lemma set_car_inc

∀s:LOSet. ∀g:OGrp.  (|oal(s;g↓hgrp)| ⊆r |oal(s;g)|)
BY
{ ((UnivCD THENA Auto) THEN RepUR ``oalist`` 0 THEN (SubtypeReasoning THENA Auto)) }

1
1. s : LOSet@i'
2. g : OGrp@i'
3. ps : (|s| × |g|+) List@i
4. ↑sd_ordered(map(λx.(fst(x));ps))@i
5. ¬↑(e ∈b map(λx.(snd(x));ps))@i
⊢ ¬↑(e ∈b map(λx.(snd(x));ps))

---

Latex:

---

Latex:
\mforall{}s:LOSet.  \mforall{}g:OGrp.    (|oal(s;g\mdownarrow{}hgrp)|  \msubseteq{}r  |oal(s;g)|)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepUR  ``oalist``  0  THEN  (SubtypeReasoning  THENA  Auto))

---

Home Index