theorem :: C0SP1:2

for V being Ring
for V1 being Subset of V st V1 is additively-closed & V1 is multiplicatively-closed & not V1 is empty holds
doubleLoopStr(# V1,(Add_ (V1,V)),(mult_ (V1,V)),(One_ (V1,V)),(Zero_ (V1,V)) #) is Ring