let x be set ; :: thesis: for N being Pnet holds
( not x in the Places of N or not x in the Transitions of N )
let N be Pnet; :: thesis: ( not x in the Places of N or not x in the Transitions of N )
the Places of N misses the Transitions of N by Def1;
hence ( not x in the Places of N or not x in the Transitions of N ) by XBOOLE_0:3; :: thesis: verum