let N be Pnet; :: thesis: for x being Element of Elements N holds Post N,x c= Elements N
let x be Element of Elements N; :: thesis: Post N,x c= Elements N
for y being set st y in Post N,x holds
y in Elements N by Def8;
hence Post N,x c= Elements N by TARSKI:def 3; :: thesis: verum