:: deftheorem defines Tempty_e_net E_SIEC:def 4 :
for X being set holds Tempty_e_net X = G_Net(# X,(id X),(id X) #);