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

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