theorem Th1: :: GRCAT_1:1

for UN being Universe
for u1, u2, u3, u4 being Element of UN holds
( [u1,u2,u3] in UN & [u1,u2,u3,u4] in UN )