let N be Pnet; :: thesis: for x being Element of Elements N holds Pre (N,x) c= Elements N

let x be Element of Elements N; :: thesis: Pre (N,x) c= Elements N

for y being object st y in Pre (N,x) holds

y in Elements N by Def6;

hence Pre (N,x) c= Elements N by TARSKI:def 3; :: thesis: verum

let x be Element of Elements N; :: thesis: Pre (N,x) c= Elements N

for y being object st y in Pre (N,x) holds

y in Elements N by Def6;

hence Pre (N,x) c= Elements N by TARSKI:def 3; :: thesis: verum