theorem :: FF_SIEC:4

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