let N be e_net; :: thesis: ( (( 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)) ~ & (( 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)) ~ )
A1: (( the entrance of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the entrance of N))) ~) = ((id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N))) ~ by RELAT_1:35
.= ( the entrance of N \ (id the carrier of N)) ~ by Th23 ;
(( the escape of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the escape of N))) ~) = ((id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N))) ~ by RELAT_1:35
.= ( the escape of N \ (id the carrier of N)) ~ by Th23 ;
hence ( (( 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)) ~ & (( 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 A1; :: thesis: verum