for UN being Universe ex x being set st
( x in UN & GO x, Trivial-addLoopStr )