:: deftheorem defines e_shore E_SIEC:def 14 :
for N being e_net holds e_shore N = the carrier of N;