let N be e_net; :: thesis: ( ( 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 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 entrance of N \ (id the carrier of N)) = {} )

set R = the entrance of N;

set S = the escape of N;

set T = id the carrier of N;

( 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:30, XBOOLE_1:36;

then A1: ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= {} by Th15;

( 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:30, XBOOLE_1:36;

then A2: ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= {} by Def2;

( 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:30, 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 Th15;

( 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:30, XBOOLE_1:36;

then ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= {} by Def2;

hence ( ( 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 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 entrance of N \ (id the carrier of N)) = {} ) by A1, A2, A3, XBOOLE_1:3; :: thesis: verum

set R = the entrance of N;

set S = the escape of N;

set T = id the carrier of N;

( 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:30, XBOOLE_1:36;

then A1: ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= {} by Th15;

( 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:30, XBOOLE_1:36;

then A2: ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= {} by Def2;

( 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:30, 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 Th15;

( 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:30, XBOOLE_1:36;

then ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= {} by Def2;

hence ( ( 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 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 entrance of N \ (id the carrier of N)) = {} ) by A1, A2, A3, XBOOLE_1:3; :: thesis: verum