theorem Th8: :: FF_SIEC:8

for M being Pnet holds
( Flow M c= [:(Elements M),(Elements M):] & (Flow M) ~ c= [:(Elements M),(Elements M):] )