---

Step * of Lemma oalist_hgrp_eqs

∀s:LOSet. ∀g:OGrp. ∀a1,a2:|oal(s;g↓hgrp)|.  ((a1 = a2 ∈ |oal(s;g)|) ⇒ (a1 = a2 ∈ |oal(s;g↓hgrp)|))
BY
{ (Auto THEN Assert ⌜strong-subtype(|oal(s;g↓hgrp)|;|oal(s;g)|)⌝⋅) }

1
.....assertion..... 
1. s : LOSet@i'
2. g : OGrp@i'
3. a1 : |oal(s;g↓hgrp)|@i
4. a2 : |oal(s;g↓hgrp)|@i
5. a1 = a2 ∈ |oal(s;g)|@i
⊢ strong-subtype(|oal(s;g↓hgrp)|;|oal(s;g)|)

2
1. s : LOSet@i'
2. g : OGrp@i'
3. a1 : |oal(s;g↓hgrp)|@i
4. a2 : |oal(s;g↓hgrp)|@i
5. a1 = a2 ∈ |oal(s;g)|@i
6. strong-subtype(|oal(s;g↓hgrp)|;|oal(s;g)|)
⊢ a1 = a2 ∈ |oal(s;g↓hgrp)|

---

Latex:

---

Latex:
\mforall{}s:LOSet.  \mforall{}g:OGrp.  \mforall{}a1,a2:|oal(s;g\mdownarrow{}hgrp)|.    ((a1  =  a2)  {}\mRightarrow{}  (a1  =  a2))


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}strong-subtype(|oal(s;g\mdownarrow{}hgrp)|;|oal(s;g)|)\mkleeneclose{}\mcdot{})

---

Home Index