PT_net_Str(# {} ,{} ,({} {} ,{} ),({} {} ,{} ) #) is Petri ;
hence ex b₁ being PT_net_Str st
( b₁ is strict & b₁ is Petri ) ; :: thesis: verum