set PLA = {0 };
consider a, b, red, yellow, blue being set ;
set TRA = {a};
set TSA = [:{a},{0 }:];
[:{a},{0 }:] c= [:{a},{0 }:] ;
then reconsider TSA = [:{a},{0 }:] as non empty Relation of , ;
set STA = [:{0 },{a}:];
[:{0 },{a}:] c= [:{0 },{a}:] ;
then reconsider STA = [:{0 },{a}:] as non empty Relation of , ;
set CS = {red,yellow,blue};
consider fa being Function of thin_cylinders {red,yellow,blue},{0 }, thin_cylinders {red,yellow,blue},{0 };
set f = {a} --> fa;
take CPNT = Colored_PT_net_Str(# {0 },{a},STA,TSA,{red,yellow,blue},({a} --> fa) #); :: thesis: ( CPNT is strict & CPNT is Colored-PT-net-like )

A1: now

{red,yellow,blue} c= {red,yellow,blue} ;
then reconsider CS1 = {red,yellow,blue} as non empty Subset of ;
let t be transition of ; :: thesis: ( t in dom the firing-rule of CPNT implies ex CS1 being non empty Subset of ex I being Subset of ex O being Subset of 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 ex I being Subset of ex O being Subset of st the firing-rule of CPNT . t is Function of thin_cylinders CS1,I, thin_cylinders CS1,O
A2: t = a by TARSKI:def 1;
A3: a in {a} by TARSKI:def 1;
A4: 0 in {0 } by TARSKI:def 1;
then [a,0 ] in TSA by A3, ZFMISC_1:106;
then 0 in {t} *' by A2, PETRI:8;
then reconsider O = {0 } as Subset of by ZFMISC_1:37;
[0 ,a] in STA by A4, A3, ZFMISC_1:106;
then 0 in *' {t} by A2, PETRI:6;
then reconsider I = {0 } as Subset of by ZFMISC_1:37;
A5: fa is Function of thin_cylinders CS1,I, thin_cylinders CS1,O ;
({a} --> fa) . t = fa by FUNCOP_1:13;
hence ex CS1 being non empty Subset of ex I being Subset of ex O being Subset of st the firing-rule of CPNT . t is Function of thin_cylinders CS1,I, thin_cylinders CS1,O by A5; :: thesis: verum

end;

A6: dom ({a} --> fa) = {a} by FUNCOP_1:19;

now

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

proof

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

end;

assume x in dom the firing-rule of CPNT ; :: thesis: x in the Transitions of CPNT \ (Outbds CPNT)
then x = a by A6, TARSKI:def 1;
hence x in the Transitions of CPNT \ (Outbds CPNT) by A8, XBOOLE_0:def 5; :: thesis: verum

end;

then dom the firing-rule of CPNT c= the Transitions of CPNT \ (Outbds CPNT) by TARSKI:def 3;
hence ( CPNT is strict & CPNT is Colored-PT-net-like ) by A1, Def10; :: thesis: verum