let N be e_net; ( e_adjac N c= [:(e_shore N),(e_shore N):] & e_flow N c= [:(e_shore N),(e_shore N):] )
A1:
(the entrance of N \/ the escape of N) \ (id the carrier of N) c= the entrance of N \/ the escape of N
by XBOOLE_1:36;
A2:
the escape of N c= [:the carrier of N,the carrier of N:]
by Def2;
A3:
the entrance of N c= [:the carrier of N,the carrier of N:]
by Def2;
then
the entrance of N ~ c= [:the carrier of N,the carrier of N:]
by SYSREL:16;
then A4:
( id the carrier of N c= [:the carrier of N,the carrier of N:] & (the entrance of N ~ ) \/ the escape of N c= [:the carrier of N,the carrier of N:] )
by A2, RELSET_1:28, XBOOLE_1:8;
( id (the carrier of N \ (rng the entrance of N)) c= id the carrier of N & id the carrier of N c= [:the carrier of N,the carrier of N:] )
by RELSET_1:28, SYSREL:33, XBOOLE_1:36;
then A5:
id (the carrier of N \ (rng the entrance of N)) c= [:the carrier of N,the carrier of N:]
by XBOOLE_1:1;
the entrance of N \/ the escape of N c= [:the carrier of N,the carrier of N:]
by A3, A2, XBOOLE_1:8;
then
(the entrance of N \/ the escape of N) \ (id the carrier of N) c= [:the carrier of N,the carrier of N:]
by A1, XBOOLE_1:1;
hence
( e_adjac N c= [:(e_shore N),(e_shore N):] & e_flow N c= [:(e_shore N),(e_shore N):] )
by A5, A4, XBOOLE_1:8; verum