let N be e_net; :: thesis: ( 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 Def1;

A3: the entrance of N c= [: the carrier of N, the carrier of N:] by Def1;

then the entrance of N ~ c= [: the carrier of N, the carrier of N:] by SYSREL:4;

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:13, 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:13, SYSREL:15, 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; :: thesis: verum

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 Def1;

A3: the entrance of N c= [: the carrier of N, the carrier of N:] by Def1;

then the entrance of N ~ c= [: the carrier of N, the carrier of N:] by SYSREL:4;

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:13, 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:13, SYSREL:15, 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; :: thesis: verum