theorem :: E_SIEC:34

for N being e_net holds
( s_post N c= [:(e_Places N),(e_Transitions N):] & s_pre N c= [:(e_Places N),(e_Transitions N):] ) by Th33;