theorem Th28: :: GRCAT_1:28

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