take N = G_Net(# {} ,{} ,{} #); :: thesis: N is EE
the entrance of N * (the entrance of N \ (id N)) = {} ;
hence N is EE by Def3; :: thesis: verum