:: deftheorem defines f_post FF_SIEC:def 14 :
for M being Pnet holds f_post M = ((Flow M) ~) | the carrier' of M;