:: deftheorem Def8 defines One_ C0SP1:def 8 :
for V being non empty multLoopStr_0
for V1 being Subset of V st V1 is multiplicatively-closed & not V1 is empty holds
One_ (V1,V) = 1. V;