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

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