for N being e_net holds
( (e_prox N) * (e_prox N) = e_prox N & ((e_prox N) \ (id (e_shore N))) * (e_prox N) = {} & ((e_prox N) \/ ((e_prox N) ~)) \/ (id (e_shore N)) = (e_flow N) \/ ((e_flow N) ~) )