:: deftheorem defines e_post E_SIEC:def 13 :
for N being e_net holds e_post N = the escape of N \ (id the carrier of N);