deffunc H₁( set ) -> Colored-PT-net = the Colored-PT-net;
consider X being ManySortedSet of I such that
A1: for d being Element of I holds X . d = H₁(d) from PBOOLE:sch 5();
take X ; :: thesis: X is Colored-PT-net-Family-like
thus X is Colored-PT-net-Family-like by A1; :: thesis: verum