let x be set ; 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; 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; ( 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
; ( x in Post (N,y) iff post N,y,x )
A2:
( post N,y,x implies x in Post (N,y) )
( 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; verum