theorem Th3: :: NECKLA_3:3

for a, b, c, d, e, f, g, h being set holds [:{a,b,c,d},{e,f,g,h}:] = {[a,e],[a,f],[b,e],[b,f],[a,g],[a,h],[b,g],[b,h]} \/ {[c,e],[c,f],[d,e],[d,f],[c,g],[c,h],[d,g],[d,h]}