let N be e_net; :: thesis: CL the entrance of N = CL the escape of N
( the entrance of N * the escape of N = the entrance of N & the escape of N * (the escape of N \ (id the carrier of N)) = {} & the escape of N * the entrance of N = the escape of N & the entrance of N * (the entrance of N \ (id the carrier of N)) = {} ) by Def2, Def3;
then ( the entrance of N * the escape of N = the entrance of N & the escape of N * (the escape of N \ (id (dom the escape of N))) = {} & the escape of N * the entrance of N = the escape of N & the entrance of N * (the entrance of N \ (id (dom the entrance of N))) = {} ) by Th16;
hence CL the entrance of N = CL the escape of N by SYSREL:59; :: thesis: verum