theorem Th1: :: YELLOW_3:1

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