theorem Th18: :: RINGCAT1:18

for UN being Universe
for x being Element of RingObjects UN holds x is strict Ring