theorem :: NET_1:13

for x being set
for N being Pnet
for y being Element of Elements N st y in the carrier' of N holds
( x in Pre (N,y) iff pre N,y,x )