set N = PetriNet ;

now :: thesis: for s being place of PetriNet holds
( ex t being transition of PetriNet st [t,s] in the T-S_Arcs of PetriNet & ( for t1, t2 being transition of PetriNet st [t1,s] in the T-S_Arcs of PetriNet & [t2,s] in the T-S_Arcs of PetriNet holds
t1 = t2 ) & ex t being transition of PetriNet st [s,t] in the S-T_Arcs of PetriNet & ( for t1, t2 being transition of PetriNet st [s,t1] in the S-T_Arcs of PetriNet & [s,t2] in the S-T_Arcs of PetriNet holds
t1 = t2 ) )

let s be place of PetriNet; :: thesis: ( ex t being transition of PetriNet st [t,s] in the T-S_Arcs of PetriNet & ( for t1, t2 being transition of PetriNet st [t1,s] in the T-S_Arcs of PetriNet & [t2,s] in the T-S_Arcs of PetriNet holds
t1 = t2 ) & ex t being transition of PetriNet st [s,t] in the S-T_Arcs of PetriNet & ( for t1, t2 being transition of PetriNet st [s,t1] in the S-T_Arcs of PetriNet & [s,t2] in the S-T_Arcs of PetriNet holds
t1 = t2 ) )
thus ex t being transition of PetriNet st [t,s] in the T-S_Arcs of PetriNet :: thesis: ( ( for t1, t2 being transition of PetriNet st [t1,s] in the T-S_Arcs of PetriNet & [t2,s] in the T-S_Arcs of PetriNet holds
t1 = t2 ) & ex t being transition of PetriNet st [s,t] in the S-T_Arcs of PetriNet & ( for t1, t2 being transition of PetriNet st [s,t1] in the S-T_Arcs of PetriNet & [s,t2] in the S-T_Arcs of PetriNet holds
t1 = t2 ) )

proof

reconsider t = 1 as transition of PetriNet by TARSKI:def 1;
take t ; :: thesis: [t,s] in the T-S_Arcs of PetriNet
thus [t,s] in the T-S_Arcs of PetriNet ; :: thesis: verum

end;

thus for t1, t2 being transition of PetriNet st [t1,s] in the T-S_Arcs of PetriNet & [t2,s] in the T-S_Arcs of PetriNet holds
t1 = t2 :: thesis: ( ex t being transition of PetriNet st [s,t] in the S-T_Arcs of PetriNet & ( for t1, t2 being transition of PetriNet st [s,t1] in the S-T_Arcs of PetriNet & [s,t2] in the S-T_Arcs of PetriNet holds
t1 = t2 ) )

proof

let t1, t2 be transition of PetriNet; :: thesis: ( [t1,s] in the T-S_Arcs of PetriNet & [t2,s] in the T-S_Arcs of PetriNet implies t1 = t2 )
assume ( [t1,s] in the T-S_Arcs of PetriNet & [t2,s] in the T-S_Arcs of PetriNet ) ; :: thesis: t1 = t2
t1 = 1 by TARSKI:def 1;
hence t1 = t2 by TARSKI:def 1; :: thesis: verum

end;

thus ex t being transition of PetriNet st [s,t] in the S-T_Arcs of PetriNet :: thesis: for t1, t2 being transition of PetriNet st [s,t1] in the S-T_Arcs of PetriNet & [s,t2] in the S-T_Arcs of PetriNet holds
t1 = t2

proof

reconsider t = 1 as transition of PetriNet by TARSKI:def 1;
take t ; :: thesis: [s,t] in the S-T_Arcs of PetriNet
thus [s,t] in the S-T_Arcs of PetriNet ; :: thesis: verum

end;

thus for t1, t2 being transition of PetriNet st [s,t1] in the S-T_Arcs of PetriNet & [s,t2] in the S-T_Arcs of PetriNet holds
t1 = t2 :: thesis: verum

proof

let t1, t2 be transition of PetriNet; :: thesis: ( [s,t1] in the S-T_Arcs of PetriNet & [s,t2] in the S-T_Arcs of PetriNet implies t1 = t2 )
assume ( [s,t1] in the S-T_Arcs of PetriNet & [s,t2] in the S-T_Arcs of PetriNet ) ; :: thesis: t1 = t2
t1 = 1 by TARSKI:def 1;
hence t1 = t2 by TARSKI:def 1; :: thesis: verum

end;

end;

hence PetriNet is decision_free_like ; :: thesis: ( PetriNet is With_directed_circuit & PetriNet is Petri )
A5: 0 in the carrier of PetriNet by TARSKI:def 1;
1 in the carrier' of PetriNet by TARSKI:def 1;
then reconsider a0 = 0 , a1 = 1 as Element of places_and_trans_of PetriNet by A5, XBOOLE_0:def 3;
reconsider fs = <*a0,a1,a0*> as FinSequence of places_and_trans_of PetriNet ;
( fs is directed_path_like & fs is circular & fs is almost-one-to-one ) by Th12, Th13;
hence PetriNet is With_directed_circuit ; :: thesis: PetriNet is Petri
Flow PetriNet c= [: the carrier of PetriNet, the carrier' of PetriNet:] \/ [: the carrier' of PetriNet, the carrier of PetriNet:] ;
hence PetriNet is Petri by NET_1:def 2, ZFMISC_1:11; :: thesis: verum