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