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