:: deftheorem defines f_enter FF_SIEC:def 7 :
for M being Pnet holds f_enter M = (((Flow M) ~) | the carrier' of M) \/ (id the carrier of M);