let N be e_net; :: thesis: ( (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; :: thesis: verum