theorem Th3: :: GRCAT_1:3

for UN being Universe holds
( {{}} in UN & [{{}},{{}}] in UN & [:{{}},{{}}:] in UN & op2 in UN & op1 in UN )