take PTN1 = TrivialPetriNet ; :: thesis: PTN1 is With_Traps
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 11 :: thesis: S is Trap-like
stf = [s,t] ;
then t in S *' ;
then {t} c= S *' by ZFMISC_1:31;
then A2: {t} = S *' ;
tsf = [t,s] ;
then t in *' S ;
hence S *' is Subset of (*' S) by A2, ZFMISC_1:31; :: according to PETRI:def 10 :: thesis: verum