theorem :: FF_SIEC:3

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