let N be e_net; :: thesis: ( (the entrance of N \ (id the carrier of N)) ~ c= [:(e_Places N),(e_Transitions N):] & (the escape of N \ (id the carrier of N)) ~ c= [:(e_Places N),(e_Transitions N):] )
( the entrance of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] & the escape of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] ) by Th24;
hence ( (the entrance of N \ (id the carrier of N)) ~ c= [:(e_Places N),(e_Transitions N):] & (the escape of N \ (id the carrier of N)) ~ c= [:(e_Places N),(e_Transitions N):] ) by SYSREL:16; :: thesis: verum