take N = G_Net(# {} ,{} ,{} #); :: thesis: N is GG
A1: the escape of N c= [:the carrier of N,the carrier of N:] by XBOOLE_1:2;
the entrance of N * the entrance of N = {} ;
hence N is GG by A1, Def2; :: thesis: verum