let x be set ; :: thesis: for N being Pnet
for y being Element of Elements N st y in the carrier' 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 carrier' of N holds
( x in Post (N,y) iff post N,y,x )
let y be Element of Elements N; :: thesis: ( y in the carrier' of N implies ( x in Post (N,y) iff post N,y,x ) )
assume A1: y in the carrier' of N ; :: thesis: ( x in Post (N,y) iff post N,y,x )
A2: ( 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 Flow N ;
then x in the carrier of N by A1, Th5;
then x in Elements N by XBOOLE_0:def 3;
hence x in Post (N,y) by A3, Def7; :: thesis: verum
end;
( x in Post (N,y) implies post N,y,x ) by Def7, A1;
hence ( x in Post (N,y) iff post N,y,x ) by A2; :: thesis: verum