let X be set ; :: thesis: ( the carrier of (Pempty_f_net X) = {} & the carrier' of (Pempty_f_net X) = X & Flow (Pempty_f_net X) = {} )
{} misses X by XBOOLE_1:65;
then Pempty_f_net X = PT_net_Str(# {},X,({} ({},X)),({} (X,{})) #) by Def4;
hence ( the carrier of (Pempty_f_net X) = {} & the carrier' of (Pempty_f_net X) = X & Flow (Pempty_f_net X) = {} ) ; :: thesis: verum