let N be e_net; :: thesis: ( the entrance of N * ( the escape of N \ (id the carrier of N)) = {} & the escape 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;
A1: the escape of N * ( the entrance of N \ (id the carrier of N)) = the escape of N * ( the entrance of N \ (id (dom the entrance of N))) by Th11
.= ( the escape of N * the entrance of N) * ( the entrance of N \ (id (dom the entrance of N))) by Def1
.= the escape of N * ( the entrance of N * ( the entrance of N \ (id (dom the entrance of N)))) by RELAT_1:36
.= the escape of N * ( the entrance of N * ( the entrance of N \ (id the carrier of N))) by Th11
.= the escape of N * {} by Def2
.= {} ;
the entrance of N * ( the escape of N \ (id the carrier of N)) = the entrance of N * ( the escape of N \ (id (dom the escape of N))) by Th11
.= ( the entrance of N * the escape of N) * ( the escape of N \ (id (dom the escape of N))) by Def1
.= the entrance of N * ( the escape of N * ( the escape of N \ (id (dom the escape of N)))) by RELAT_1:36
.= the entrance of N * ( the escape of N * ( the escape of N \ (id the carrier of N))) by Th11
.= the entrance of N * {} by Def2
.= {} ;
hence ( the entrance of N * ( the escape of N \ (id the carrier of N)) = {} & the escape of N * ( the entrance of N \ (id the carrier of N)) = {} ) by A1; :: thesis: verum