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