theorem :: FF_SIEC:5

for x being object holds
( the carrier of (Psingle_f_net x) = {x} & the carrier' of (Psingle_f_net x) = {} & Flow (Psingle_f_net x) = {} )