:: deftheorem Def7 defines Post NET_1:def 7 :
for N being PT_net_Str
for x being Element of Elements N
for b₃ being set holds
( b₃ = Post (N,x) iff for y being object holds
( y in b₃ iff ( y in Elements N & [x,y] in Flow N ) ) );