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