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;
A: [#] ({{}},{{}}) = {[{},{}]} by ZFMISC_1:35;
then reconsider stf = [{},{}] as S-T_arc of PTN1 by TARSKI:def 1;
reconsider tsf = [{},{}] as T-S_arc of PTN1 by TARSKI:def 1, A;
{{}} 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:37;
then A1: {t} = S *' by XBOOLE_0:def 10;
tsf = [t,s] ;
then t in *' S ;
hence S *' is Subset of (*' S) by A1, ZFMISC_1:37; :: according to PETRI:def 10 :: thesis: verum