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 the carrier of N) = (the entrance of N ~ ) \ ((id the carrier of N) ~ ) by RELAT_1:72
.= (the entrance of N \ (id the carrier of N)) ~ by RELAT_1:41 ;
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 Th24, XBOOLE_1:42;
the entrance of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] by Th24;
then (the entrance of N ~ ) \ (id the carrier of N) c= [:(e_Places N),(e_Transitions N):] by A1, SYSREL:16;
hence e_Flow N c= [:(e_Places N),(e_Transitions N):] \/ [:(e_Transitions N),(e_Places N):] by A2, XBOOLE_1:13; :: thesis: verum