theorem SYLM2: :: PETRI_3:4
for I being non trivial finite set
for CPNT being Colored-PT-net-Family of I holds not union { (Funcs ((Outbds (CPNT . i)), the carrier of (CPNT . j))) where i, j is Element of I : i <> j } is empty