let N be e_net; ( (id ( the carrier of N \ (rng the escape of N))) * (( the escape of N \ (id the carrier of N)) ~) = {} & (id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) ~) = {} )
A1: (id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) ~) =
((id ( the carrier of N \ (rng the entrance of N))) ~) * (( the entrance of N \ (id the carrier of N)) ~)
by RELAT_1:72
.=
(( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) ~
by RELAT_1:54
.=
{}
by Th35, RELAT_1:66
;
(id ( the carrier of N \ (rng the escape of N))) * (( the escape of N \ (id the carrier of N)) ~) =
((id ( the carrier of N \ (rng the escape of N))) ~) * (( the escape of N \ (id the carrier of N)) ~)
by RELAT_1:72
.=
(( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))) ~
by RELAT_1:54
.=
{}
by Th35, RELAT_1:66
;
hence
( (id ( the carrier of N \ (rng the escape of N))) * (( the escape of N \ (id the carrier of N)) ~) = {} & (id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) ~) = {} )
by A1; verum