theorem :: NET_1:8

for x, y being set
for N being Pnet st [x,y] in Flow N & y in the carrier of N holds
x in the carrier' of N