{} in {{} } by TARSKI:def 1;
then reconsider f = {[{} ,{} ]} as non empty Relation of {{} },{{} } by RELSET_1:8;
take PTN1 = PT_net_Str(# {{} },{{} },f,f #); :: 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;
reconsider stf = [{} ,{} ] as S-T_arc of PTN1 by TARSKI:def 1;
reconsider tsf = [{} ,{} ] as T-S_arc of PTN1 by TARSKI:def 1;
{{} } c= the Places of PTN1 ;
then reconsider S = {{} } as Subset of the Places of PTN1 ;
take S ; :: according to PETRI:def 6 :: thesis: S is Deadlock-like
tsf = [t,s] ;
then t in *' S ;
then {t} c= *' S by ZFMISC_1:37;
then A1: {t} = *' S by XBOOLE_0:def 10;
stf = [s,t] ;
then t in S *' ;
hence *' S is Subset of (S *' ) by A1, ZFMISC_1:37; :: according to PETRI:def 5 :: thesis: verum