let N be e_net; :: thesis: ( (the escape of N \ (id the carrier of N)) * (the escape of N \ (id the carrier of N)) = {} & (the entrance of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N)) = {} & (the escape of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of 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)) * (the escape of N \ (id the carrier of N)) c= the escape of N * (the escape of N \ (id the carrier of N)) by RELAT_1:49, XBOOLE_1:36;
then A1: (the escape of N \ (id the carrier of N)) * (the escape of N \ (id the carrier of N)) c= {} by Def3;
(the entrance of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N)) c= the entrance of N * (the entrance of N \ (id the carrier of N)) by RELAT_1:49, XBOOLE_1:36;
then A2: (the entrance of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N)) c= {} by Def3;
(the escape of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N)) c= the escape of N * (the entrance of N \ (id the carrier of N)) by RELAT_1:49, XBOOLE_1:36;
then A3: (the escape of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N)) c= {} by Th20;
(the entrance of N \ (id the carrier of N)) * (the escape of N \ (id the carrier of N)) c= the entrance of N * (the escape of N \ (id the carrier of N)) by RELAT_1:49, XBOOLE_1:36;
then (the entrance of N \ (id the carrier of N)) * (the escape of N \ (id the carrier of N)) c= {} by Th20;
hence ( (the escape of N \ (id the carrier of N)) * (the escape of N \ (id the carrier of N)) = {} & (the entrance of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N)) = {} & (the escape of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N)) = {} & (the entrance of N \ (id the carrier of N)) * (the escape of N \ (id the carrier of N)) = {} ) by A1, A2, A3, XBOOLE_1:3; :: thesis: verum