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 consider t being transition of PTN such that
x = t and
A1: ex f being S-T_arc of PTN ex s being place of PTN st
( s in {} the Places of PTN & f = [s,t] ) ;
consider f being S-T_arc of PTN, s being place of PTN such that
A2: ( s in {} the Places of PTN & f = [s,t] ) by A1;
thus contradiction by A2; :: thesis: verum