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 S-T_arc of PTN ex t being transition of PTN st
( t in {} the carrier' of PTN & f = [s,t] ) ) ;
hence contradiction ; :: thesis: verum