:: deftheorem defines empty_e_net E_SIEC:def 3 :
empty_e_net = G_Net(# {},{},{} #);