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