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