Step
*
of Lemma
oal_lv_wf
∀s:LOSet. ∀g:AbDMon. ∀ps:|oal(s;g)|.  ((¬(ps = 00 ∈ |oal(s;g)|)) 
⇒ (lv(ps) ∈ |g|))
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}s:LOSet.  \mforall{}g:AbDMon.  \mforall{}ps:|oal(s;g)|.    ((\mneg{}(ps  =  00))  {}\mRightarrow{}  (lv(ps)  \mmember{}  |g|))
By
Latex:
ProveWfLemma
Home
Index