set PLA = {0};
set a = the set ;
set TRA = { the set };
set TSA = [:{ the set },{0}:];
[:{ the set },{0}:] c= [:{ the set },{0}:] ;
then reconsider TSA = [:{ the set },{0}:] as non empty Relation of { the set },{0} ;
set STA = [:{0},{ the set }:];
[:{0},{ the set }:] c= [:{0},{ the set }:] ;
then reconsider STA = [:{0},{ the set }:] as non empty Relation of {0},{ the set } ;
set CS = { the set , the set , the set };
set fa = the Function of (thin_cylinders ({ the set , the set , the set },{0})),(thin_cylinders ({ the set , the set , the set },{0}));
set f = { the set } --> the Function of (thin_cylinders ({ the set , the set , the set },{0})),(thin_cylinders ({ the set , the set , the set },{0}));
set CPNT = Colored_PT_net_Str(# {0},{ the set },STA,TSA,{ the set , the set , the set },({ the set } --> the Function of (thin_cylinders ({ the set , the set , the set },{0})),(thin_cylinders ({ the set , the set , the set },{0}))) #);
A1: Colored_PT_net_Str(# {0},{ the set },STA,TSA,{ the set , the set , the set },({ the set } --> the Function of (thin_cylinders ({ the set , the set , the set },{0})),(thin_cylinders ({ the set , the set , the set },{0}))) #) is with_S-T_arc ;
Colored_PT_net_Str(# {0},{ the set },STA,TSA,{ the set , the set , the set },({ the set } --> the Function of (thin_cylinders ({ the set , the set , the set },{0})),(thin_cylinders ({ the set , the set , the set },{0}))) #) is with_T-S_arc ;
then reconsider CPNT = Colored_PT_net_Str(# {0},{ the set },STA,TSA,{ the set , the set , the set },({ the set } --> the Function of (thin_cylinders ({ the set , the set , the set },{0})),(thin_cylinders ({ the set , the set , the set },{0}))) #) as Colored_Petri_net by A1;
take CPNT ; :: thesis: ( CPNT is strict & CPNT is Colored-PT-net-like )

A2: now :: thesis: for t being transition of CPNT st t in dom the firing-rule of CPNT holds
ex CS1 being non empty Subset of the ColoredSet of CPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT . t is Function of (thin_cylinders (CS1,I)),(thin_cylinders (CS1,O))

{ the set , the set , the set } c= { the set , the set , the set } ;
then reconsider CS1 = { the set , the set , the set } as non empty Subset of the ColoredSet of CPNT ;
let t be transition of CPNT; :: thesis: ( t in dom the firing-rule of CPNT implies ex CS1 being non empty Subset of the ColoredSet of CPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT . t is Function of (thin_cylinders (CS1,I)),(thin_cylinders (CS1,O)) )
assume t in dom the firing-rule of CPNT ; :: thesis: ex CS1 being non empty Subset of the ColoredSet of CPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT . t is Function of (thin_cylinders (CS1,I)),(thin_cylinders (CS1,O))
A3: t = the set by TARSKI:def 1;
A4: the set in { the set } by TARSKI:def 1;
A5: 0 in {0} by TARSKI:def 1;
then [ the set ,0] in TSA by A4, ZFMISC_1:87;
then 0 in {t} *' by A3, PETRI:8;
then reconsider O = {0} as Subset of ({t} *') by ZFMISC_1:31;
[0, the set ] in STA by A5, A4, ZFMISC_1:87;
then 0 in *' {t} by A3, PETRI:6;
then reconsider I = {0} as Subset of (*' {t}) by ZFMISC_1:31;
A6: the Function of (thin_cylinders ({ the set , the set , the set },{0})),(thin_cylinders ({ the set , the set , the set },{0})) is Function of (thin_cylinders (CS1,I)),(thin_cylinders (CS1,O)) ;
({ the set } --> the Function of (thin_cylinders ({ the set , the set , the set },{0})),(thin_cylinders ({ the set , the set , the set },{0}))) . t = the Function of (thin_cylinders ({ the set , the set , the set },{0})),(thin_cylinders ({ the set , the set , the set },{0})) by FUNCOP_1:7;
hence ex CS1 being non empty Subset of the ColoredSet of CPNT ex I being Subset of (*' {t}) ex O being Subset of ({t} *') st the firing-rule of CPNT . t is Function of (thin_cylinders (CS1,I)),(thin_cylinders (CS1,O)) by A6; :: thesis: verum

end;

A7: dom ({ the set } --> the Function of (thin_cylinders ({ the set , the set , the set },{0})),(thin_cylinders ({ the set , the set , the set },{0}))) = { the set } by FUNCOP_1:13;

now :: thesis: for x being object st x in dom the firing-rule of CPNT holds
x in the carrier' of CPNT \ (Outbds CPNT)

reconsider a1 = the set as transition of CPNT by TARSKI:def 1;
let x be object ; :: thesis: ( x in dom the firing-rule of CPNT implies x in the carrier' of CPNT \ (Outbds CPNT) )
0 in {0} by TARSKI:def 1;
then [a1,0] in TSA by ZFMISC_1:87;
then A8: not {a1} *' = {} by PETRI:8;
A9: not a1 in Outbds CPNT

proof

assume a1 in Outbds CPNT ; :: thesis: contradiction
then ex x being transition of CPNT st
( a1 = x & x is outbound ) ;
hence contradiction by A8; :: thesis: verum

end;

assume x in dom the firing-rule of CPNT ; :: thesis: x in the carrier' of CPNT \ (Outbds CPNT)
then x = the set by A7, TARSKI:def 1;
hence x in the carrier' of CPNT \ (Outbds CPNT) by A9, XBOOLE_0:def 5; :: thesis: verum

end;

then dom the firing-rule of CPNT c= the carrier' of CPNT \ (Outbds CPNT) ;
hence ( CPNT is strict & CPNT is Colored-PT-net-like ) by A2; :: thesis: verum