theorem :: E_SIEC:20

for N being e_net holds
( e_pre N c= [:(e_Transitions N),(e_Places N):] & e_post N c= [:(e_Transitions N),(e_Places N):] ) by Th18;