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