:: deftheorem defines Pempty_e_net E_SIEC:def 5 :
for X being set holds Pempty_e_net X = G_Net(# X,{},{} #);