:: deftheorem defines e_entrance E_SIEC:def 17 :
for N being e_net holds e_entrance N = (( the escape of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the escape of N)));