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