for N being Pnet
for X being Subset of (Elements N)
for x being Element of Elements N st Elements N <> {} holds
( x in Output (N,X) iff ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st
( y in X & y in the carrier' of N & post N,y,x ) ) )