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