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:35
.=
{}
by Th24, RELAT_1:43
;
(( 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:35
.=
{}
by Th24, RELAT_1:43
;
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