theorem Th4: :: FUNCT_5:10

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