take PTN1 = TrivialPetriNet ; :: thesis: PTN1 is With_Deadlocks
reconsider s = {} as place of PTN1 by TARSKI:def 1;
reconsider t = {} as transition of PTN1 by TARSKI:def 1;
A1: [#] ({{}},{{}}) = {[{},{}]} by ZFMISC_1:29;
then reconsider stf = [{},{}] as S-T_arc of PTN1 by TARSKI:def 1;
reconsider tsf = [{},{}] as T-S_arc of PTN1 by A1, TARSKI:def 1;
{{}} c= the carrier of PTN1 ;
then reconsider S = {{}} as Subset of the carrier of PTN1 ;
take S ; :: according to PETRI:def 9 :: thesis: S is Deadlock-like
tsf = [t,s] ;
then t in *' S ;
then {t} c= *' S by ZFMISC_1:31;
then A2: {t} = *' S ;
stf = [s,t] ;
then t in S *' ;
hence *' S is Subset of (S *') by A2, ZFMISC_1:31; :: according to PETRI:def 8 :: thesis: verum