:: deftheorem defines field NET_1:def 10 :
for N being Pnet
for x being Element of Elements N holds field (N,x) = (enter (N,x)) \/ (exit (N,x));