for M being Pnet holds
( dom (f_escape M) c= Elements M & rng (f_escape M) c= Elements M & dom (f_entrance M) c= Elements M & rng (f_entrance M) c= Elements M )