theorem Th33: :: E_SIEC:33

for N being e_net holds
( ( 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):] )