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