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