let PTN be PT_net_Str ; :: thesis: ({} the Places of PTN) *' = {}
consider x being Element of ({} the Places of PTN) *' ;
assume not ({} the Places of PTN) *' = {} ; :: thesis: contradiction
then x in ({} the Places of PTN) *' ;
then ex t being transition of PTN st
( x = t & ex f being S-T_arc of PTN ex s being place of PTN st
( s in {} the Places of PTN & f = [s,t] ) ) ;
hence contradiction ; :: thesis: verum