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