theorem Th14: :: CARDFIL4:15

for A being Subset of [:NAT,NAT:] holds proj1 A = { x where x is Element of NAT : ex y being Element of NAT st [x,y] in A }