let x be set ; :: thesis: for N being Pnet
for y being Element of Elements N st y in the Transitions of N holds
( x in Post N,y iff post N,y,x )
let N be Pnet; :: thesis: for y being Element of Elements N st y in the Transitions of N holds
( x in Post N,y iff post N,y,x )
let y be Element of Elements N; :: thesis: ( y in the Transitions of N implies ( x in Post N,y iff post N,y,x ) )
assume A1: y in the Transitions of N ; :: thesis: ( x in Post N,y iff post N,y,x )
A2: ( x in Post N,y implies post N,y,x )

proof

assume x in Post N,y ; :: thesis: post N,y,x
then [y,x] in the Flow of N by Def8;
hence post N,y,x by A1, Def6; :: thesis: verum

end;

( post N,y,x implies x in Post N,y )

proof

assume post N,y,x ; :: thesis: x in Post N,y
then A3: [y,x] in the Flow of N by Def6;
then x in the Places of N by A1, Th12;
then x in Elements N by XBOOLE_0:def 3;
hence x in Post N,y by A3, Def8; :: thesis: verum

end;

hence ( x in Post N,y iff post N,y,x ) by A2; :: thesis: verum