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