:: deftheorem defines Psingle_e_net E_SIEC:def 6 :
for x being object holds Psingle_e_net x = G_Net(# {x},(id {x}),(id {x}) #);