let N be e_net; ( ((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)) ~ ) = {} )
A1: ((the entrance 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 entrance of N \ (id the carrier of N))) ~
by RELAT_1:54
.=
{}
by Th32, RELAT_1:66
;
((the escape 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 escape of N \ (id the carrier of N))) ~
by RELAT_1:54
.=
{}
by Th32, RELAT_1:66
;
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)) ~ ) = {} )
by A1; verum