:: deftheorem defines e_pre E_SIEC:def 12 :
for N being e_net holds e_pre N = the entrance of N \ (id the carrier of N);