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 ) ; :: thesis: verum