theorem Th13: :: E_SIEC:13

for N being e_net holds
( rng the entrance of N = rng (CL the entrance of N) & rng the entrance of N = dom (CL the entrance of N) & rng the escape of N = rng (CL the escape of N) & rng the escape of N = dom (CL the escape of N) & rng the entrance of N = rng the escape of N )