let N be e_net; ( ( 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; verum