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