theorem Th16: :: RINGCAT1:16

for UN being Universe ex x being object st
( x in UN & GO x, Z_3 )