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