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)) = {} )

set T = the entrance of N;

set C = the carrier of N;

set E = the escape of N;

set I = id the carrier of N;

( 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 A1: ( the entrance of N \ (id the carrier of N)) * ( the entrance 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 A2: ( 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 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 A3: ( 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 ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= {} by Def2;

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

set T = the entrance of N;

set C = the carrier of N;

set E = the escape of N;

set I = id the carrier of N;

( 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 A1: ( the entrance of N \ (id the carrier of N)) * ( the entrance 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 A2: ( 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 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 A3: ( 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 ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= {} by Def2;

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