theorem Th5: :: FUNCT_5:11

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