theorem Th15: :: CARDFIL4:16

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