let N be e_net; ( e_prox N c= [:(e_shore N),(e_shore N):] & e_flow N c= [:(e_shore N),(e_shore N):] )
A1:
id the carrier of N c= [: the carrier of N, the carrier of N:]
by RELSET_1:13;
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:
( the entrance of N ~) \/ the escape of N c= [: the carrier of N, the carrier of N:]
by A2, XBOOLE_1:8;
the entrance of N \/ the escape of N c= [: the carrier of N, the carrier of N:]
by A3, A2, XBOOLE_1:8;
hence
( e_prox N c= [:(e_shore N),(e_shore N):] & e_flow N c= [:(e_shore N),(e_shore N):] )
by A4, A1, SYSREL:4, XBOOLE_1:8; verum