:: deftheorem defines PTempty_e_net E_SIEC:def 8 :
for X, Y being set holds PTempty_e_net (X,Y) = G_Net(# (X \/ Y),(id X),(id X) #);