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