:: deftheorem defines Postc NET_1:def 12 :
for N being PT_net_Str
for x being Element of the carrier' of N
for b₃ being set holds
( b₃ = Postc (N,x) iff for y being object holds
( y in b₃ iff ( y in the carrier of N & [x,y] in Flow N ) ) );