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