:: deftheorem Def5 defines Add_ C0SP1:def 5 :
for V being non empty addLoopStr
for V1 being Subset of V st V1 is add-closed & not V1 is empty holds
Add_ (V1,V) = the addF of V || V1;