theorem Th3: :: E_SIEC:3

for X being set holds G_Net(# X,(id X),(id X) #) is e_net