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