let X be set ; :: thesis: G_Net(# X,(id X),(id X) #) is e_net
A1: (id X) * ((id X) \ (id X)) = (id X) * {} by XBOOLE_1:37
.= {} ;
( id X c= [:X,X:] & (id X) * (id X) = id X ) by RELSET_1:13, SYSREL:12;
hence G_Net(# X,(id X),(id X) #) is e_net by A1, Def1, Def2; :: thesis: verum