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

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