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