theorem :: FF_SIEC:20

for M being Pnet holds
( (f_exit M) * ((f_exit M) \ (id (Elements M))) = {} & (f_enter M) * ((f_enter M) \ (id (Elements M))) = {} )