let X be set ; :: thesis: G_Net(# X,{},{} #) is e_net
( {} c= [:X,X:] & {} * ({} \ (id X)) = {} ) by XBOOLE_1:2;
hence G_Net(# X,{},{} #) is e_net by Def1, Def2; :: thesis: verum