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