:: deftheorem defines s_post E_SIEC:def 21 :
for N being G_Net holds s_post N = ( the entrance of N \ (id the carrier of N)) ~ ;