for x being set
for N being Pnet holds
( not x in the carrier of N or not x in the carrier' of N ) by Def2, XBOOLE_0:3;