let N be e_net; ( 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 )
the entrance of N * (the entrance of N \ (id the carrier of N)) = {}
by Def3;
then A1:
the entrance of N * (the entrance of N \ (id (dom the entrance of N))) = {}
by Th16;
the escape of N * (the escape of N \ (id the carrier of N)) = {}
by Def3;
then A2:
the escape of N * (the escape of N \ (id (dom the escape of N))) = {}
by Th16;
A3:
the escape of N * the escape of N = the escape of N
by Def2;
then A4:
rng the escape of N = rng (CL the escape of N)
by A2, SYSREL:50;
A5:
the entrance of N * the entrance of N = the entrance of N
by Def2;
then
rng the entrance of N = rng (CL the entrance of N)
by A1, SYSREL:50;
hence
( 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 )
by A5, A1, A3, A2, A4, Th17, SYSREL:50; verum