:: deftheorem defines multiplicatively-closed C0SP1:def 4 :
for V being non empty multLoopStr_0
for V1 being Subset of V holds
( V1 is multiplicatively-closed iff ( 1. V in V1 & ( for v, u being Element of V st v in V1 & u in V1 holds
v * u in V1 ) ) );