for X, Y, Z being set st Z c= [:X,Y:] holds
( proj1 Z c= X & proj2 Z c= Y )