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