let N be e_net; :: thesis: CL the entrance of N = CL the escape of N
the escape of N * ( the escape of N \ (id N)) = {} by Def2;
then A1: the escape of N * ( the escape of N \ (id (dom the escape of N))) = {} by Th11;
the entrance of N * ( the entrance of N \ (id N)) = {} by Def2;
then A2: the entrance of N * ( the entrance of N \ (id (dom the entrance of N))) = {} by Th11;
( the entrance of N * the escape of N = the entrance of N & the escape of N * the entrance of N = the escape of N ) by Def1;
hence CL the entrance of N = CL the escape of N by A1, A2, SYSREL:40; :: thesis: verum