for M being Pnet holds
( (f_escape M) * ((f_escape M) \ (id (Elements M))) = {} & (f_entrance M) * ((f_entrance M) \ (id (Elements M))) = {} )