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

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