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

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; :: thesis: verum