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