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