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 ;
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 ;
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 ;
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 ;
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 ; :: thesis: verum