:: deftheorem defines e_prox E_SIEC:def 15 :
for N being e_net holds e_prox N = ( the entrance of N \/ the escape of N) ~ ;