{} 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_Traps
{{} } c= the Places of PTN1 ;
then reconsider S = {{} } as Subset of the Places of PTN1 ;
take S ; :: according to PETRI:def 8 :: thesis: S is Trap-like
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;
( stf = [s,t] & s in S ) ;
then t in S *' ;
then {t} c= S *' by ZFMISC_1:37;
then A1: {t} = S *' by XBOOLE_0:def 10;
( tsf = [t,s] & s in S ) ;
then t in *' S ;
hence S *' is Subset of (*' S) by A1, ZFMISC_1:37; :: according to PETRI:def 7 :: thesis: verum