let PTN be Petri_net; :: thesis: ({} the carrier' of PTN) *' = {}
set x = the Element of ({} the carrier' of PTN) *' ;
assume not ({} the carrier' of PTN) *' = {} ; :: thesis: contradiction
then the Element of ({} the carrier' of PTN) *' in ({} the carrier' of PTN) *' ;
then ex s being place of PTN st
( the Element of ({} the carrier' of PTN) *' = s & ex f being T-S_arc of PTN ex t being transition of PTN st
( t in {} the carrier' of PTN & f = [t,s] ) ) ;
hence contradiction ; :: thesis: verum