theorem :: FF_SIEC:2

for X being set holds
( the carrier of (Tempty_f_net X) = X & the carrier' of (Tempty_f_net X) = {} & Flow (Tempty_f_net X) = {} )