empty_f_net = Net(# {} ,{} ,{} #) by Def4, XBOOLE_1:65;
hence ( the Places of empty_f_net = {} & the Transitions of empty_f_net = {} & the Flow of empty_f_net = {} ) ; :: thesis: verum