let N be e_net; :: thesis: e_Flow N c= [:(e_Places N),(e_Transitions N):] \/ [:(e_Transitions N),(e_Places N):]
A1: ( the entrance of N ~) \ (id N) = ( the entrance of N ~) \ ((id the carrier of N) ~)
.= ( the entrance of N \ (id the carrier of N)) ~ by RELAT_1:24 ;
A2: ( e_Flow N = (( the entrance of N ~) \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N)) & the escape of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] ) by Th18, XBOOLE_1:42;
the entrance of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] by Th18;
then ( the entrance of N ~) \ (id the carrier of N) c= [:(e_Places N),(e_Transitions N):] by A1, SYSREL:4;
hence e_Flow N c= [:(e_Places N),(e_Transitions N):] \/ [:(e_Transitions N),(e_Places N):] by A2, XBOOLE_1:13; :: thesis: verum